proposition: Lemma inner_swap_hexagon'_3 (x y z : V) : inner_swap x x y y #⊗ identity (z ⊗ z) · inner_swap (x ⊗ y) (x ⊗ y) z z · mon_lassociator _ _ _ #⊗ mon_lassociator _ _ _ = mon_lassociator _ _ _ · identity (x ⊗_ x) #⊗ inner_swap y y z z · inner_swap x x (y ⊗ z) (y ⊗ z).
proof: Proof. apply inner_swap_hexagon'. 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