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](http://cs.nyu.edu/pipermail/fom/2008-March/012783.html) 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.



Category theory without axiom of choice
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](http://homotopytypetheory.org/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](https://ncatlab.org/nlab/show/transfinite+construction+of+free+algebras) 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.


