theorem EGNO.MacLaneCoherence.macLane_coherence_free (C : Type u_1) : Quiver.IsThin (CategoryTheory.FreeMonoidalCategory C)

The free monoidal category on a set of objects is a thin category: between any two parenthesized products there is at most one morphism. This is the core form of MacLane's coherence theorem.

def EGNO.MacLaneCoherence.macLane_coherence_normalization (C : Type u_1) : CategoryTheory.Functor.id (CategoryTheory.FreeMonoidalCategory C) ≅ (CategoryTheory.FreeMonoidalCategory.fullNormalize C).comp CategoryTheory.FreeMonoidalCategory.inclusion

The full normalization isomorphism in the free monoidal category, witnessing that every object is canonically isomorphic to its normalized form.

theorem EGNO.MacLaneCoherence.Theorem_1_9_1 {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.MonoidalCategory D] (f : C → D) {P₁ P₂ : CategoryTheory.FreeMonoidalCategory C} (g₁ g₂ : P₁ ⟶ P₂) : (CategoryTheory.FreeMonoidalCategory.project f).map g₁ = (CategoryTheory.FreeMonoidalCategory.project f).map g₂

Theorem 1.9.1 (MacLane's Coherence Theorem): Any two morphisms built by composing associativity and unit isomorphisms (and their inverses, possibly tensored with identities) between the same source and target in a monoidal category are equal.