Lemma sym_monoidal_braiding_hexagon1_variant (y z w : V) : mon_rassociator y z w · (sym_mon_braiding _ y z ⊗^{V}_{r} w · mon_lassociator z y w) = sym_mon_braiding _ _ _ · mon_lassociator _ _ _ · _ ⊗^{V}_{l} sym_mon_braiding _ _ _. Proof. rewrite assoc. apply pathsinv0. use (z_iso_inv_to_right _ _ _ _ (_ ,, _)). { use (is_z_iso_leftwhiskering_z_iso V). apply is_z_isomorphism_sym_mon_braiding. } cbn. rewrite ! assoc'. etrans. 2: { apply maponpaths. rewrite assoc. refine (sym_mon_hexagon_lassociator V _ _ _ @ _). rewrite <- (when_bifunctor_becomes_rightwhiskering V). now rewrite <- (when_bifunctor_becomes_leftwhiskering V). } rewrite ! assoc. etrans. 2: { do 2 apply maponpaths_2. apply pathsinv0, monoidal_associatorisolaw. } 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.