# mathlibdocumentation

category_theory.monoidal.unitors

# The two morphisms λ_ (𝟙_ C) and ρ_ (𝟙_ C) from 𝟙_ C ⊗ 𝟙_ C to 𝟙_ C are equal.

This is suprisingly difficult to prove directly from the usual axioms for a monoidal category!

This proof follows the diagram given at https://people.math.osu.edu/penneys.2/QS2019/VicaryHandout.pdf

It should be a consequence of the coherence theorem for monoidal categories (although quite possibly it is a necessary building block of any proof).

theorem category_theory.monoidal_category.unitors_equal.cells_9 {C : Type u}  :
(α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom 𝟙 (𝟙_ C) = (α_ (𝟙_ C 𝟙_ C) (𝟙_ C) (𝟙_ C)).hom (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C 𝟙_ C)).hom (𝟙 (𝟙_ C) (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).inv) (α_ (𝟙_ C) (𝟙_ C 𝟙_ C) (𝟙_ C)).inv

theorem category_theory.monoidal_category.unitors_equal.cells_10_13 {C : Type u}  :
((ρ_ (𝟙_ C 𝟙_ C)).inv 𝟙 (𝟙_ C)) (α_ (𝟙_ C 𝟙_ C) (𝟙_ C) (𝟙_ C)).hom (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C 𝟙_ C)).hom (𝟙 (𝟙_ C) (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).inv) (α_ (𝟙_ C) (𝟙_ C 𝟙_ C) (𝟙_ C)).inv = (𝟙 (𝟙_ C) (ρ_ (𝟙_ C)).inv 𝟙 (𝟙_ C))