proposition: 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: 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.
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