I am learning category theory from Bartosz's blog, where he mentioned that:
If the product exists for any pair of objects, the mapping from those objects to the product is bifunctorial.
Based on my understanding, product is unique only up to isomorphism, which means for an object $(X, Y)$ in the product category $C \times C$, there could be multiple (mutually isomorphic) objects (along with their projection morphisms) serving as the product $X \times Y$. However, according to the definition of functor,
a functor $F: C \rightarrow D$ associates each object X in C an object F(X) in D.
which does not align with Bartosz's statement unless multiple isomorphic objects can be considered as an object F(X) in the definition.
So my question is whether Bartosz's statement about the bifunctoriality is correct? If it is correct, what part am I missing? If it's not, what assumptions/restrictions is he missing (or implying).
This is a real technicality, albeit one that isn't usually an issue. If you have some construction of coproducts, then it is usually easy to show that it is bifunctorial. Often we equip categories with chosen coproducts, meaning we explicitly provide a bifunctor. However, in general, knowing that some category has all coproducts doesn't provide you with a bifunctor for the reason you state. The Axiom of Choice (or some variant) can be used to create such a bifunctor. An approach to avoid the Axiom of Choice (besides having an explicit construction, which, again, you often do) is to use the notion of anafunctors instead of functors. This notion was specifically formulated to deal with the necessity for the Axiom of Choice in other context, specifically equivalence of categories.
When one says that a category has coproducts, often this is treated as having chosen coproducts. Of course, there's nothing special about coproducts in the any of this, and anything characterized by a universal property has similar issues.