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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Import BifunctorNotations. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Import MonoidalNotations.