Lemma inner_swap_hexagoninv' (x y z : V) : identity (x ⊗ x) #⊗ inner_swap y y z z · inner_swap x x (y ⊗ z) (y ⊗ z) · mon_rassociator _ _ _ #⊗ mon_rassociator _ _ _ = mon_rassociator _ _ _ · inner_swap x x y y #⊗ identity (z ⊗ z) · inner_swap (x ⊗ y) (x ⊗ y) z z. Proof. set (t := inner_swap_hexagon' x x y y z z). apply pathsinv0. use (z_iso_inv_on_left _ _ _ _ (mon_lassociator _ _ _ #⊗ mon_lassociator _ _ _,, mon_rassociator _ _ _ #⊗ mon_rassociator _ _ _ ,, _)). { apply (pr2 (is_z_iso_bifunctor_z_iso V (mon_lassociator _ _ _) (mon_lassociator _ _ _) (_ ,, monoidal_associatorisolaw V _ _ _) (_ ,, monoidal_associatorisolaw V _ _ _))). } cbn. etrans. 2: { rewrite ! assoc'. apply maponpaths. rewrite assoc. apply (! t). } etrans. 2: { rewrite ! assoc. do 2 apply maponpaths_2. apply pathsinv0. apply mon_rassociator_lassociator. } now rewrite id_left. 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.