Excellent solutions to Puzzle 280, folks! I guess it was a bit sadistic to assign this without mentioning that \$$\rho_I = \lambda_I\$$.

Anindya wrote:

> This is listed in Mac Lane as one of the coherence equations, although more recent treatments seem to omit it. I'm assuming this because it can be derived from the other two equations ("pentagon" and "triangle").

Yes, right now I'm forgetting who first noticed that this can be derived from the other ones.

A more reasonable definition of monoidal category might say that _all_ diagrams built using tensor products, composition, \$$I\$$, \$$\alpha\$$, \$$\rho\$$ and \$$\lambda\$$ commute. While trimming down this infinite set of equations to the bare minimum is nice, using this bare minimum as the definition of monoidal category makes this concept look rather mysterious at first.

However, correctly stating that "all diagrams built using tensor products, composition, \$$I\$$, \$$\alpha\$$, \$$\rho\$$ and \$$\lambda\$$ commute" is actually a bit tricky: if you say this the wrong way it will be false.

So, people state the bare minimum set of equations - Mac Lane had three but nowadays we use just two: the "pentagon" and "triangle". Then, **Mac Lane's coherence theorem** says these imply all the rest. Here's a precise statement, and sketch of the proof:

* nLab, [Mac Lane's proof of the coherence theorem for monoidal categories](https://ncatlab.org/nlab/show/Mac+Lane%27s+proof+of+the+coherence+theorem+for+monoidal+categories).

It's a pretty technical inductive argument. But this page does give a nice explanation of why a naive formulation of "all diagrams built using tensor products, composition, \$$I\$$, \$$\alpha\$$, \$$\rho\$$ and \$$\lambda\$$ commute" doesn't actually work.