proposition: Lemma mon_rassociator_inner_swap (x y z w : V) : mon_rassociator _ _ _ · inner_swap x y z w · mon_rassociator _ _ _ = (identity _ ) #⊗ mon_rassociator _ _ _ · mon_rassociator _ _ _ · ((identity _ ) #⊗ (sym_mon_braiding V y z) · mon_rassociator _ _ _) #⊗ (identity _ ).
proof: Proof. unfold inner_swap. rewrite !assoc. rewrite mon_rassociator_lassociator. rewrite id_left. rewrite !assoc'. rewrite tensor_mor_left. rewrite tensor_comp_id_l. rewrite !assoc'. apply maponpaths. etrans. { apply maponpaths. apply mon_rassociator_rassociator. } rewrite tensor_comp_id_r. rewrite !assoc. apply maponpaths_2. rewrite <- tensor_comp_id_l. etrans. { rewrite assoc'. apply maponpaths_2. do 2 apply maponpaths. apply mon_lassociator_rassociator. } rewrite id_right. rewrite tensor_mor_right. apply tensor_rassociator. 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