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.
