## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorMike Shulman
• CommentTimeApr 27th 2019

Clarified the relationship between anafunctions and graphs (thanks for the pointer).

• CommentRowNumber2.
• CommentAuthorsamwinnick
• CommentTimeDec 20th 2022
• (edited Dec 20th 2022)

This article references a context in which the “axiom of unique choice” fails, (which I am not familiar with), but I am wondering about how or whether the usual axiom of choice comes into play here. I recently learned from the page on anafunctors that there is a way to circumvent the axiom of choice in proving the forward direction of the following statement, and this is to use anafunctors in place of functors:

a functor is fully faithful and essentially surjective if and only if it is (part of) an equivalence.

If I understand correctly, this page on anafunction basically argues that (in a typical setup, say ZF) one does not need anafunctions, because this point doesn’t matter in Set as it did in Cat, since in Set, the forward direction “every bijection is an isomorphism” does not require AC, since we recover the inverse of f from the converse of the graph of f. While this is true, the situation pertaining to injections and embeddings is different. The statement “every injection has a left inverse” (as well as the statement “every surjection has a right inverse”) requires AC.

Question 1: Does the notion of “anafunction” eliminate the need for AC here? If it does, does this mean that “anafunction” is actually a useful concept, say in ZF?

Actually, I am interested in a slightly different characterization of “embedding” in Set than “having a left inverse”, (but I guess it might be equivalent to “having a left inverse” even without AC so the slight difference is perhaps not so important). I am not as interested in characterizing it as “having a left inverse” because this is not how embeddings work in Cat, and ultimately, I am only here to get intuition on the notion of anafunctor as it pertains to embeddings in Cat. Consider the following two “factorization properties” of Set:

i. Every function $f:X\to Y$ can be written as $f=i\circ f'$ where $i:Y'\to Y$ is an inclusion and $f':X\to Y'$ is surjective, and

ii. $f$ is injective if and only if $f'$ is a bijective.

Since the image of a functor is not necessarily a category, statement i does not “categorify” to a statement about Cat, but ii does, and this shows how one must define “embedding of categories” to get a statement analogous to “f is an injection iff f is an embedding”, namely:

a functor is fully faithful if and only if it is an embedding

where I would call $F:A\to B$ an embedding if there is a natural isomorphism $F\cong I\circ F'$, where $I:B'\to B$ is an inclusion functor, and $F'$ lies in an equivalence $(F,G,\eta,\epsilon)$.

Again the forward direction requires AC, but this time so does the analogous statement about Set. So the notion of “embedding” I am focusing on for Set is basically point ii above: say $f$ is an embedding if $f=i\circ f'$ where $i$ is an inclusion and $f'$ is an isomorphism.

Question 2: Does the notion of “anafunction” fix this? Ie. make it so that the statement “every injection is an embedding” no longer require choice, (with “embedding” as I just defined)?

If it would be preferable for me to ask this somewhere else like stackexchange or something please let me know. Thank you!

• Mike Shulman, Mathematics without the principle of unique choice. Mathoverflow. Jun 5, 2018. (web

Anonymous

• CommentRowNumber4.
• CommentAuthorDmitri Pavlov
• CommentTimeDec 21st 2022

Fixed the broken link.

2. starting section on anafunctions in dependent type theory

Anonymous

• CommentRowNumber6.
• CommentAuthorUrs
• CommentTimeJan 5th 2023
• (edited Jan 5th 2023)

hyperlinked more of the technical terms (e.g. type family and categorical semantics)

where you write of “elements” of a type I hyperlinked to term

where you had references to “dependent type theory” I suppose it needs “homotopy type theory” or at least “Martin-Löf dependent type theory”, for definiteness, and so I added that, with hyperlinks.

• CommentRowNumber7.
• CommentAuthorDavidRoberts
• CommentTimeJan 7th 2023

“Every injection with inhabited domain and decidable codomain has a left inverse” is true without AC. You can even drop the assumption of decidability on the codomain, as long as the image is complenented.