proposition: Lemma inner_swap_inv (x y z w : V) : inner_swap x y z w · inner_swap x z y w = identity _.
proof: Proof. unfold inner_swap. apply pathsinv0. rewrite ! assoc'. use (z_iso_inv_to_left _ _ _ (_ ,, _)). { apply (_ ,, monoidal_associatorisolaw V _ _ _). } cbn. rewrite ! assoc. use (z_iso_inv_on_left _ _ _ _ (mon_lassociator _ _ _ ,, mon_rassociator _ _ _ ,, _)). { apply (_ ,, monoidal_associatorisolaw _ _ _ _). } cbn. rewrite id_right. etrans. 2: { apply pathsinv0. apply monoidal_associatorisolaw. } cbn. etrans. { apply maponpaths_2. rewrite assoc'. apply maponpaths. apply monoidal_associatorisolaw. } rewrite id_right. refine (! bifunctor_leftcomp V _ _ _ _ _ _ @ _). etrans. { apply maponpaths. rewrite assoc'. apply maponpaths. rewrite ! assoc. do 2 apply maponpaths_2. apply monoidal_associatorisolaw. } rewrite id_left. etrans. { apply maponpaths. rewrite assoc. apply maponpaths_2. rewrite assoc'. apply maponpaths. refine (! bifunctor_rightcomp V _ _ _ _ _ _ @ _). apply maponpaths. apply (monoidal_braiding_inverses V). } rewrite (bifunctor_rightid V). rewrite id_right. etrans. { apply maponpaths. apply monoidal_associatorisolaw. } apply (bifunctor_leftid V). 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