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.