proposition: Proposition mon_lassociator_lassociator {w x y z : V} : mon_lassociator (w ⊗ x) y z · mon_lassociator w x (y ⊗ z) = mon_lassociator w x y #⊗ identity z · mon_lassociator w (x ⊗ y) z · identity w #⊗ mon_lassociator x y z.
proof: Proof. refine (!(monoidal_pentagonidentity V w x y z) @ _). unfold monoidal_cat_tensor_mor. unfold functoronmorphisms1. rewrite (bifunctor_rightid V). rewrite (bifunctor_leftid V). rewrite !id_left, id_right. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Equivalences.FullyFaithful UniMath.CategoryTheory.opp_precat