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}
[category_theory.category C]
[category_theory.monoidal_category C] :
theorem
category_theory.monoidal_category.unitors_equal.cells_10_13
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C] :
theorem
category_theory.monoidal_category.unitors_equal
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C] :