Lemma inner_swap_commute_with_swap (x1 x2 y1 y2 : V) : inner_swap x1 x2 y1 y2 · sym_mon_braiding _ x1 y1 #⊗ sym_mon_braiding _ x2 y2 = sym_mon_braiding _ (x1 ⊗ x2) (y1 ⊗ y2) · inner_swap y1 y2 x1 x2. Proof. unfold inner_swap. rewrite ! assoc. etrans. 2: { do 2 apply maponpaths_2. apply pathsinv0, sym_mon_tensor_lassociator0. } unfold monoidal_cat_tensor_mor, mon_lassociator, mon_rassociator. cbn. etrans. 2: { apply maponpaths_2. rewrite assoc'. apply maponpaths. rewrite (when_bifunctor_becomes_leftwhiskering V). etrans. 2: apply (bifunctor_leftcomp V y1). apply maponpaths. rewrite ! assoc. apply pathsinv0. apply sym_mon_hexagon_rassociator0. } etrans. 2: { rewrite ! assoc'. do 2 apply maponpaths. refine (! sym_mon_hexagon_lassociator1 _ _ _ _ _ @ _). now rewrite ! assoc'. } unfold functoronmorphisms1. rewrite ! assoc. apply maponpaths_2. unfold monoidal_cat_tensor_pt. cbn. rewrite ! assoc'. apply pathsinv0. use (z_iso_inv_on_right _ _ _ (mon_lassociator _ _ _ ,, mon_rassociator _ _ _ ,, _)). { apply monoidal_associatorisolaw. } cbn. rewrite (bifunctor_leftcomp V). rewrite ! assoc. etrans. 2: { do 3 apply maponpaths_2. apply pathsinv0. apply mon_lassociator_lassociator'. } rewrite (bifunctor_leftid V). rewrite id_right. apply pathsinv0. use (z_iso_inv_to_right _ _ _ _ (_ ,, _)). { use (is_z_iso_rightwhiskering_z_iso V). refine (_ ,, _). apply (_ ,, monoidal_braiding_inverses V). } cbn. etrans. 2: { rewrite assoc'. apply maponpaths. apply pathsinv0, monoidal_associatornatright. } etrans. 2: { rewrite assoc. apply maponpaths_2. rewrite <- ! (bifunctor_rightcomp V). apply maponpaths. apply pathsinv0, sym_mon_hexagon_rassociator1. } rewrite ! (bifunctor_rightcomp V). rewrite ! assoc'. apply maponpaths. rewrite ! assoc. rewrite (bifunctor_leftcomp V). rewrite assoc. unfold sym_mon_braiding, mon_lassociator, monoidal_cat_tensor_pt. cbn. rewrite (monoidal_associatornatleftright V). rewrite ! assoc'. apply maponpaths. rewrite assoc. apply pathsinv0. use (z_iso_inv_on_left _ _ _ _ (mon_lassociator _ _ _ ,, mon_rassociator _ _ _ ,, _)). { apply monoidal_associatorisolaw. } cbn. rewrite assoc'. etrans. 2: { apply maponpaths. apply pathsinv0, mon_lassociator_lassociator. } unfold monoidal_cat_tensor_mor. unfold mon_lassociator. unfold mon_rassociator. unfold monoidal_cat_tensor_pt. cbn. rewrite ! assoc. rewrite (when_bifunctor_becomes_rightwhiskering V). rewrite <- (bifunctor_rightcomp V). etrans. 2: { do 2 apply maponpaths_2. apply maponpaths. apply pathsinv0, (monoidal_associatorisolaw V). } rewrite (bifunctor_rightid V). rewrite id_left. now rewrite (when_bifunctor_becomes_leftwhiskering V). 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.