Conditional on chapter 3 returning "weak". The associator is a 2-morphism, and Mac Lane's coherence theorem says that one condition on it — the pentagon — is enough to make every bracketing of every composite canonically equal. That is the first genuinely 2-categorical statement the series would own.
With four operators there are five bracketings of the full chain, and the associator relates them pairwise. Mac Lane's theorem is that if the pentagon identity holds among those five, then all diagrams built from associators commute, and an unbracketed expression like G = U∘F∘K∘C denotes a well-defined morphism after all. Without it, the expression is ambiguous and the ambiguity is invisible.
The pentagon is a statement about four composable morphisms. With three you can write the associator but nothing constrains it. With four the constraint appears, and it is the first place a chain can be incoherent. The series has four operators. This is not a coincidence to be celebrated — it is the reason the question could not be avoided.
| Needed | Mathlib path | Files |
|---|---|---|
| Bicategories, associator, pentagon | CategoryTheory/Bicategory/ | 44 |
| Monoidal coherence | CategoryTheory/Monoidal/ | 108 |
| Base category theory | CategoryTheory/ | 1089 |
Measured on the Mathlib built in the geometry repository, 2026-08-29. The pentagon is already formalised; this chapter would instantiate it, not prove it. DATA
The associator written explicitly for this chain, and the
pentagon either verified in Lean against CategoryTheory.Bicategory or shown to fail.
A failure would be the more interesting outcome and must not be quietly dropped.