“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.

]]>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.

]]>starting section on anafunctions in dependent type theory

Anonymous

]]>Fixed the broken link.

]]>adding reference

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

Anonymous

]]>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!

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

]]>