MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).
    Post Made Community Wiki by Scott Morrison
show/hide this revision's text 1

Using the usual definition of "functor," almost any functor constructed using only universal properties requires the axiom of choice. For instance, if a category C has products, then one wants a "product assigning" functor C×C → C, but in order to define this you have to choose a product for each pair of objects. If C is a large category, then you need an axiom of choice for proper classes.

However, this sort of thing is arguably not a "real" use of the axiom of choice. It's more accurate to say that in the absence of the axiom of choice the usual definition of "functor" is not sufficient, and one must use anafunctors instead. Proving that fully faithful + essentially surjective = equivalence is the same. Most often in category theory when we want to "choose" something, that thing is in fact determined up to unique isomorphism (though not uniquely on the nose) and in that case using anafunctors is sufficient to avoid choice.

The axiom of choice does, however, come up in the study of particular properties of the category Set. One interesting consequence of the fact that epics split in Set is that all functors defined on Set preserve epics. I think this is an important part of Blass' proof that the existence of nontrivial (left and right) exact endofunctors of set is equivalent to the existence of measurable cardinals. Another interesting consequence is that Set is its own "ex/lex completion."