Lemma naturality_inner_swap {x y z w : V} {x' y' z' w' : V} (fx : V⟦x,x'⟧) (fy : V⟦y,y'⟧) (fz : V⟦z,z'⟧) (fw : V⟦w,w'⟧) : inner_swap x y z w · ((fx #⊗ fz) #⊗ (fy #⊗ fw)) = ((fx #⊗ fy) #⊗ (fz #⊗ fw)) · inner_swap _ _ _ _. Proof. unfold inner_swap. etrans. { rewrite ! assoc'. do 2 apply maponpaths. apply pathsinv0. exact (monoidal_associatorinv_nat2 V fx fz (fy #⊗ fw)). } rewrite ! assoc. apply maponpaths_2. etrans. 2: { apply maponpaths_2. apply associator_nat2. } rewrite ! assoc'. apply maponpaths. etrans. { apply maponpaths_2. apply maponpaths. apply (sym_monoidal_braiding_hexagon1_variant y z w). } rewrite <- ! (when_bifunctor_becomes_leftwhiskering V). refine (! tensor_comp_mor _ _ _ _ @ _). refine (_ @ tensor_comp_mor _ _ _ _ ). rewrite id_left, id_right. apply maponpaths. etrans. 2: { apply maponpaths. exact (! sym_monoidal_braiding_hexagon1_variant y' z' w'). } rewrite ! assoc. etrans. 2: { do 2 apply maponpaths_2. apply pathsinv0, tensor_sym_mon_braiding. } rewrite ! assoc'. apply maponpaths. unfold monoidal_cat_tensor_mor. cbn. rewrite ! assoc. etrans. 2: { apply maponpaths_2. apply associator_nat2. } rewrite ! assoc'. apply maponpaths. refine (! tensor_comp_mor _ _ _ _ @ _). rewrite id_left. etrans. { apply maponpaths. apply pathsinv0, tensor_sym_mon_braiding. } cbn. rewrite <- (when_bifunctor_becomes_leftwhiskering V). refine (_ @ tensor_comp_mor _ _ _ _). apply maponpaths_2. apply pathsinv0, id_right. 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.