Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-01 18:03 d3c565d4

View on Github →

feat(category_theory/monoidal): the monoidal coherence theorem (#7324) This PR contains a proof of the monoidal coherence theorem, stated in the following way: if C is any type, then the free monoidal category over C is a preorder. This should immediately imply the statement needed in the coherence branch.

Estimated changes