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. 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.
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.