Lemmas which are consequences of monoidal coherence #

These lemmas are all proved by coherence.

Future work #

Investigate whether these lemmas are really needed, or if they can be replaced by use of the coherence tactic.

theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor''_assoc {C : Type u_1} [] (X : C) (Y : C) {Z : C} (h : ) :
theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor' {C : Type u_1} [] (X : C) (Y : C) :
theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv'_assoc {C : Type u_1} [] (X : C) (Y : C) {Z : C} (h : ) :
theorem CategoryTheory.MonoidalCategory.id_tensor_rightUnitor_inv_assoc {C : Type u_1} [] (X : C) (Y : C) {Z : C} (h : ) :
theorem CategoryTheory.MonoidalCategory.leftUnitor_inv_tensor_id_assoc {C : Type u_1} [] (X : C) (Y : C) {Z : C} (h : ) :
theorem CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom_assoc {C : Type u_1} [] (W : C) (X : C) (Y : C) (Z : C) {Z : C} :
theorem CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom {C : Type u_1} [] (W : C) (X : C) (Y : C) (Z : C) :
theorem CategoryTheory.MonoidalCategory.unitors_equal {C : Type u_1} [] :
().hom = ().hom
theorem CategoryTheory.MonoidalCategory.pentagon_hom_inv {C : Type u_1} [] {W : C} {X : C} {Y : C} {Z : C} :
theorem CategoryTheory.MonoidalCategory.pentagon_inv_hom {C : Type u_1} [] (W : C) (X : C) (Y : C) (Z : C) :