Mac Lane's coherence theorem

Remarks

Proof idea for part 1: every word can be moved by a formal morphism to a normal form. For example, the normal form can put all brackets to the right and remove all copies of $I$. One shows that any two such moves to normal form are equal, using the pentagon identity and the triangle identity to compare the possible first steps. Then any formal morphism $u \to v$ equals the composite of the move $u \to$ normal form and the inverse of the move $v \to$ normal form. Equivalently, the free monoidal category on a set of variables is a preorder.

The word "formal" is necessary. A diagram of instances of $\alpha$, $\lambda$, $\rho$ on actual objects may fail to commute. This can happen when the diagram only makes sense because two different words give equal objects, for example when $A \otimes B = C$ holds in $\mathcal{C}$. Formal diagrams track each variable, so such accidental identifications are not allowed.

Going deeper

For a student

Coherence is what makes calculations in monoidal categories practical: it justifies string diagrams and the habit of pretending that the tensor product is strictly associative. It reduces infinitely many coherence conditions to the two axioms of the definition, the pentagon and the triangle. For braided monoidal categories the analogous statement says that formal diagrams commute when they have the same underlying braid; for symmetric ones, when they have the same underlying permutation.