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. apply inner_swap_hexagon'. 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.