Defining Functors when there are Choices Involved I'm a little confused about how we formally define functors in certain instances, namely when there is no canonical choice for precisely which object of the target category we send each object in the source category to. This sounds a little vague, so I'll go by way of examples.

*

*The functor $\operatorname{Hom}(\bullet,B)$ from the category of abelian groups to itself. I have no issue here; Given an abelian group $A$, there is a well defined set $\operatorname{Hom}(A,B)$ which is given an abelian group structure.


*The functor $\bullet \otimes B$. This gives me a little more trouble, since there are many equivalent ways of defining the tensor product $A \otimes B$. Formally a functor has to send $A$ to a precise abelian group, not a class of abelian groups. Do we just make an arbitrary choice for every single possible $A$ and call it a day? This doesn't really sit right with me, but since there's a specific way the tensor product is usually defined (as a quotient of a free abelian group), this isn't that big of a deal to me.


*The functors Ext and Tor. These pose a real problem for me, since the exact group the functors assign to a pair of abelian groups depends on the choice of free (or injective for the case of Ext) resolution we go with. Sure there are canonical equivalences between all the possible resultant groups, but there's no canonical way of choosing each one. If a functor is supposed to assign a single target object to each source object, how do we go about making that choice?
I was initially thinking that the axiom of choice could let us pick an arbitrary target object for each source object, but in general the class of objects isn't even a set, so the axiom of choice can only be used for small categories.
 A: You're exactly right that, to turn certain constructions into functors, we need an axiom of global choice, that is, an axiom of choice for classes: a product of and class of nonempty classes is nonempty. For a simple example, given an arbitrary large category $\mathcal C$ which admits products and a fixed object $c$ of $\mathcal C$, the axiom of global choice is needed to construct a functor $c\times (-):\mathcal C\to \mathcal C$ assigning to every $c'\in \mathcal C$ a product $c\times c'$.
In the most common foundations used in category theory, this is no problem. Typically one might use Grothendieck universes, in which every large category becomes small in an appropriate universe, and then this global axiom of choice reduces to the usual one together with a large cardinal axiom. Alternatively one might use NBG set theory, which directly axiomatizes both sets and classes and implies no new statements about sets beyond ZFC. There we explicitly assume there exists a global choice function, namely a function from the class of all nonempty classes to itself choosing an element of every nonempty class.
In a more constructive paradigm, it's more appropriate to modify the definitions so that, for instance, for a category to admit products means for it to come equipped with chosen product functors. Alternatively, one can consider anafunctors, which are generalizations of functors which are intended to precisely model the notion of a functor that's well defined only up to canonical isomorphism.
In practice, no matter the approach taken, there is never any serious gap between an anafunctor and a functor, and most mathematicians pay no notice whatsoever to issues like those you describe, even in the case of derived functors and other elaborate constructions involving numerous choices. As long as the choices are unique up to canonical isomorphism, they are almost never distinguished from choices that are literally unique. A final foundational framework in which this practical perspective is realized most closely is in homotopy type theory, where the notions of equality and of canonical isomorphism become precisely the same. This is, to my mind, the correct attitude toward such issues.
