proposition: Lemma mon_lassociator_inner_swap (x y z w : V) : mon_lassociator _ _ _ · inner_swap x y z w · mon_lassociator _ _ _ = mon_lassociator _ _ _ #⊗ (identity _ ) · mon_lassociator _ _ _ · (identity _ ) #⊗ (sym_mon_braiding V y z #⊗ (identity _ ) · mon_lassociator _ _ _).
proof: Proof. unfold inner_swap. rewrite !assoc. rewrite mon_lassociator_lassociator. rewrite !assoc'. do 2 apply maponpaths. etrans. { do 2 apply maponpaths. apply mon_rassociator_lassociator. } rewrite id_right. rewrite tensor_mor_left. rewrite <- tensor_comp_id_l. apply maponpaths. etrans. { rewrite !assoc. do 2 apply maponpaths_2. apply mon_lassociator_rassociator. } rewrite id_left. rewrite tensor_mor_right. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Structure.Symmetric