Confusion over functors regarding universal objects

Let $\mathcal C$ be a category and suppose it has all finite products. I want to show that there is a functor $- \times - \colon \mathcal C \times \mathcal C \to \mathcal C$ which sends $(A,B)$ to the product $A \times B$ (as part of proving that $\mathcal C$ is a monoidal category). However there are possibly lots of choices of products of $A$ and $B$, so I guess the only way this makes sense is for each pair $(A,B)$ is to pick one product structure $A \times B$. However am I allowed to do this with the axiom of choice? Surely it is possible there are a massive amount of objects I have to choose a product structure on (e.g. one for each set, and so having to choose a product structure for every element in a proper class)?

Obviously this question will generalise to other notions such as choosing a specific tensor product etc. Thanks for any help.

-
Mmm... axiom of global choice... – Asaf Karagila Sep 1 '12 at 20:14
I have been told that replacing functors with anafunctors (ncatlab.org/nlab/show/anafunctor) is one way to deal with this. – Qiaochu Yuan Sep 1 '12 at 21:27
@Paul: If the only thing you're told is "products exist", then you can't say there is a product bifunctor. But that doesn't stop a product bifunctor from existing for categories you know more about, such as Set, or any context that starts with "Let $\mathcal{C}$ be a category with a product bifunctor...." – Hurkyl Sep 1 '12 at 23:39
Some authors work around the problem by redefining the phrase "category with products/limits". For example, one could say "$\mathcal{C}$ has limits of shape $\mathcal{J}$ iff the insertion-of-constants $\Delta : \mathcal{C} \to [\mathcal{J}, \mathcal{C}]$ has a right adjoint." – Zhen Lin Sep 2 '12 at 0:26
ok. I am happy to accept global choice since it seems to be needed to prove that two categories are equivalent iff there is a full and faithful functor between them (to define the functor you need to make a choice for each element in the object class) – Paul Slevin Sep 2 '12 at 15:27

I'm not a category expert and these issues use to freak me out, but let's see: according to Mac Lane, a category consists of a set of objects, right?

So, all of your isomorphism classes $A\times B$ (consisting of all objects satisfying the universal property of the produt) cannot have more than a set of objects, right?

Hence, you have a family of sets (all the isomorphisms classes of products $A\times B$, for each pair of objects $A,B$ in your category), and you pick one object of each set.

Isn't that exactly the axiom of choice?

-
But we want to be able to say, for example, that the category of sets has a product functor, and the objects in $\text{Set}$ don't form a set. – Qiaochu Yuan Sep 1 '12 at 21:20
@QiaochuYuan. As I've said, I'm not an expert on foundational issues, but always according to Mac Lane, the category of (small) sets has as objects all the sets belonging to a "big enough" set (yes) $U$, the universe, which, time and again, Mac Lane says it's a set. – a.r. Sep 1 '12 at 21:44
Okay, but if you take the universe approach then you need to assume more than the axiom of choice to do anything, namely in practice you need to assume some version of the existence of universes, which is independent of ZFC (en.wikipedia.org/wiki/Grothendieck_universe). – Qiaochu Yuan Sep 1 '12 at 21:47
In addition to what Qiaochu said above, you can force global choice without adding new sets to a universe of ZFC. It means that requiring global choice from the start has no additional costs, in contrast to universes. – Asaf Karagila Sep 1 '12 at 22:28
I insist that I'm not an expert on these foundation issues, but if Wikipedia doesn't lie to us, en.wikipedia.org/wiki/Axiom_of_global_choice , the global axiom of choice cannot be stated as such in ZFC, or just for a explicit class. So: how could be applied in this case? – a.r. Sep 1 '12 at 22:38