# Category theory without axiom of choice

I'm looking for references on the development of (some of) Category theory without the axiom of choice. One possible axiom system (that, to me, seems the natural setting) is ZF + there are arbitrarily large inaccessible cardinals.

I found a link to these notes by Solovay somewhere in mathoverflow, that I can't seem to find now. It gives a notion of inaccessible cardinals ("v-inaccessible" in the text) that can be formulated in ZF. And the existance of arbitrary large such cardinals does not imply AC (this is the first example in the notes), but is still equivalent (over ZF) to axiom of "every set belongs to a Grothendieck universe", which means that, theoretically [1], category theory can be done in such set theory.

Are there any such texts/papers?

[1] What I mean is that there are no foundational obstructions.

• – Alec Rhea Oct 27 '17 at 10:35
• Are you familiar with Makkai's paper "Avoiding the axiom of choice in general category theory" ? It is a bit orthogonal to what you mention in your question (As far as I remember it does not discuss universe) but it develop very good notions which avoid all those anoying problems of having to chose limits and so one... – Simon Henry Oct 27 '17 at 10:35
• Yes, but I'm saying that the focus on universes is a bit irrelevant. It's just a small observation. There are other things which require the use of choice, in an actual and substantial way. Universes are entirely boring. Yes, you need to formulate exactly what you mean by an inaccessible... hurray... what else is new in the choiceless world? – Asaf Karagila Oct 27 '17 at 12:20
• @OmerRosler : roughly yes, more precesely an anafunctor is something to which object $c \in C$ attach a 'set' (even a class in some cases) of objects $F(c) \rightarrow D$ with canonical isomorphism between each of these objects (and the action on morphims as well). for example if you want to define the anafunctor $C \times C \rightarrow C$ which to each pairs of objects $C$ associate their products then you just associate the set of all possible products and their canonical isomorphisms between them instead of having to 'chose' one product for each pair. The theory works very nicely... – Simon Henry Oct 27 '17 at 13:05
• ... The only place where you are getting into trouble is that without some very weak choice principles (discussed at the end of the paper. you end up with the fact that the category of anafunctors between two small category may fails to be small it self (see mathoverflow.net/questions/264585/… ) – Simon Henry Oct 27 '17 at 13:07

As was pointed out in a comment (that should have been an answer), Makkai's work on anafunctors gives a way to replace the notion of "functor" by a more general notion that doesn't require the axiom of choice in order to prove, for instance, that every fully faithful essentially surjective functor is an equivalence (in the sense of having an inverse up to isomorphism), or that if every pair of objects have a cartesian product then there is a product-assigning functor. However, as was also pointed out in a comment, this doesn't work perfectly inside ZF: in particular the category of anafunctors between two small categories may no longer be small, unless you assume extra axioms. It's also kind of tedious to work explicitly with anafunctors everywhere, which may be why no one has tried to push Makkai's work much further.

Another approach to choice-free category theory is to decide to live with the fact that not every fully faithful essentially surjective functor is an equivalence (i.e. not every "weak equivalence" is a "strong equivalence"), and define a category to (for instance) "have products" if there is a functor assigning a product to every pair of objects rather than merely that a product exists for every pair of objects. This generally works quite well too; although in general, objects with universal properties are only determined up to isomorphism, in practice it seems that (at least when doing category theory based on set theory) nearly all objects with universal properties can in fact be constructed functorially without assuming choice. For instance, in the category of sets there is a cartesian product functor defined by using "the" definition of cartesian products (e.g. Kuratowski ordered pairs), and almost any way of constructing a new category from others that inherits limits or colimits will preserve their functorial nature without using choice. A reference that uses this approach pretty systematically is Peter Johnstone's Sketches of an Elephant, which conveniently also includes one of the rare sort of cases where it doesn't work (section D1.5).

A third way of dealing with this problem is to use "saturated" or "univalent" categories in homotopy type theory; see chapter 9 of the homotopy type theory book. In this context, one can prove that if "essentially unique" objects (e.g. with universal properties) exist, then there is always a functor selecting them, even without assuming the axiom of choice: it's a higher-categorical version of the "unique choice principle" which doesn't depend on the axiom of choice.

Finally, this is not actually the only use of choice in category theory. In particular, transfinite induction is sometimes used to construct free algebras, left adjoints, cofibrant replacements, and so on, especially when working with locally presentable categories. This is actually a "real" use of choice, as such free algebras may not exist at all in ZF; this was shown by Andreas Blass in his paper Words, free algebras, and coequalizers. I don't know of a good way to deal with this in ZF, but in homotopy type theory one can often use higher inductive types to construct such things.

• It's also kind of tedious to work explicitly with anafunctors everywhere, which may be why no one has tried to push Makkai's work much further. <--- I re-read Makkai's paper recently, and there's so much in there that is "it can be checked" and "the reader can show", becuase proving things about eg the self-enriched bicategory of small categories and anafunctors is long. It's the kind of thing that made Voevodsky worried, because the effort required to do the checking thoroughly is discouraging, to say the least. – theHigherGeometer Oct 28 '17 at 0:18