Proof that a Cartesian category is monoidal

Question

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:
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?

Answer 1

There is a complete proof formalised by Scott Morrison in the Lean proof assistant here:

monoidal/of_has_finite_products.lean

[UPDATE] Here is some commentary. In the above file, we see

variables (C : Type u) [category.{v} C] {X Y : C}

In ordinary mathematical language, this means roughly as follows:

Let $C$ be a set in the Grothendieck universe $u$. Suppose we have a category structure on $C$, i.e. a category with object set $C$; the hom sets are in the Grothendieck universe $v$. Let $X$ and $Y$ be objects of $C$.

This is slightly inaccurate because Lean is based on type theory rather than set theory, and $u$ and $v$ are not really Grothendieck universes but they play the same sort of role in avoiding Russell-type paradoxes.

Later we see

def monoidal_of_has_finite_products [has_terminal C] [has_binary_products C] : monoidal_category C :=
{ tensor_unit  := ⊤_ C,
  tensor_obj   := λ X Y, X ⨯ Y,
  tensor_hom   := λ _ _ _ _ f g, limits.prod.map f g,
  associator   := prod.associator,
  left_unitor  := λ P, prod.left_unitor P,
  right_unitor := λ P, prod.right_unitor P,
  pentagon'    := prod.pentagon,
  triangle'    := prod.triangle,
  associator_naturality' := @prod.associator_naturality _ _ _, }
end

This can be translated as follows:

Suppose that $C$ also has a terminal object and binary products. Then we define a monoidal category structure on $C$, which we call monoidal_of_has_finite_products C, as follows: the tensor unit is the terminal object, the tensor product of two objects X and Y is X ⨯ Y, the tensor product of morphisms is given by the function limits.prod.map that was defined elsewhere, ...

Most of the ingredients used here are actually defined in the file binary_products.lean. For example, in that file we see

lemma prod.pentagon [has_binary_products C] (W X Y Z : C) :
  prod.map ((prod.associator W X Y).hom) (𝟙 Z) ≫
      (prod.associator W (X ⨯ Y) Z).hom ≫ prod.map (𝟙 W) ((prod.associator X Y Z).hom) =
    (prod.associator (W ⨯ X) Y Z).hom ≫ (prod.associator W X (Y ⨯ Z)).hom :=
by simp

The symbol ≫ used here is just backwards composition, i.e. f ≫ g = g o f. Everything before the := is the statement of the pentagon lemma, and after the := we have the proof, which is just by simp. Earlier in this file, and in other files, there are many lemmas marked with @[simp]. The directive by simp just tells Lean to try to apply any such lemmas that are applicable, and in this case, that is enough to complete the proof.

Answer 2

In Categories for the Working Mathematician, the first thing that Mac Lane does after defining a monoidal category in Ch. VII.1 is to verify that a category with finite products is monoidal. The associator and unitors were constructed and verified to be natural earlier in the book, in Prop III.5.1, so all that remains for Mac Lane to do is to verify that the coherence diagrams commute. He does this in sketch form only, indicating that one should check on product projections. But this is probably as explicit a verification as you'll find in the literature.

You may find more explicit verification of stronger claims. For instance, Selinger discusses in his Survey of graphical languages for monoidal categories, Sec 6.1 the fact that a cartesian monoidal category may be defined as a symmetric monoidal category where every object has a commutative comonoid structure and every morphism is a comonoid homomorphism and $\otimes$ preserves counits and comultiplications. He doesn't explicitly prove this, but perhaps somebody has worked this out in detail somewhere else.

Answer 3

One can find a completely explicit, constructive proof of this in the agda-categories library too, with explicit equational proofs for all pieces. There's an html version for easy web readability too (go to the almost bottom of that file). The symmetric monoidal category is worked out too.

The advantage of doing it this way is that, if you ever wonder why some specific detail is true, it's all here to be seen. No details omitted.