Proof that a Cartesian category is monoidal

category-theorymonoidal-categories

If $\mathcal C$ is a category with products and a terminal object, then $\mathcal C$ is monoidal.

This seems obvious, but wherever I look for a proof or a reference it simply states that the proof is "pretty involved".
I found this 8 years old question on MathOverflow:
https://mathoverflow.net/questions/111193/monoidal-structure-on-a-category-with-products-and-with-terminal-object

The answer given there uses the fact that Set is monoidal, along with the Yoneda lemma.
Is there any other reference that proves it more "generally" (i.e without resorting to Set), or a standard reference?

Best Answer

To define the product functor we need to fix a binary product, together with the projections, for each pair of objects.
The first thing to verify here is that it indeed defines a functor, i.e. uniquely determines the image of any pair of morphisms (in a functorial way).

I guess, the most problematic parts of the statement are the coherence conditions.

To get the proof smoother, let's also fix ternary and quarternary products (and nullary product as fixing the terminal object $1$, and unary products with the identity as projection).

For example, if we write $(a\times b\times c)\times d$, that is a binary product whose first term is a ternary product, and by the universal property we can easily see that it has a unique isomorphism from the quarternary product $a\times b\times c\times d$ that commutes with our fixed projections.
Similarly, for any act of 'putting in a pair of parenthesis' into a product of objects there belongs a unique isomorphism.

Now we define the associators $\alpha_{a,b,c}$ as the composite $(a\times b)\times c\longleftarrow a\times b\times c\longrightarrow a\times (b\times c)$ of the above isomorphisms.

Once again using the universal property of products, one can prove that if we put two pairs of parentheses in a product through the above isomorphisms, then the order doesn't matter: we'll receive commutative squares (like in the picture below).

To conclude the coherence pentagon condition, I found this picture among my old notes (on Leinster's unbiased bicategories), where the product sign $\times$ is omitted (so for example the top arrow is read as $((a\times b)\times c)\times d\overset{\alpha_{a,b,c}\times d}\longrightarrow (a\times(b\times c))\times d$).
The coherence conditions for unit are similar but easier, they might be thought as the case when we put an empty pair of parentheses into a product, like in "$ab\to ab()$" which would mean $a\times b\longrightarrow a\times b\times 1$.

Coherence pentagon