Lemma inner_swap_hexagon' (x1 x2 y1 y2 z1 z2 : V) : inner_swap x1 x2 y1 y2 #⊗ identity (z1 ⊗ z2) · inner_swap (x1 ⊗ y1) (x2 ⊗ y2) z1 z2 · mon_lassociator _ _ _ #⊗ mon_lassociator _ _ _ = mon_lassociator _ _ _ · identity (x1 ⊗ x2) #⊗ inner_swap y1 y2 z1 z2 · inner_swap x1 x2 (y1 ⊗ z1) (y2 ⊗ z2). Proof. refine (!(id_right _) @ _). rewrite <- inner_swap_inv. rewrite !assoc. apply maponpaths_2. refine (!(id_right _) @ _). etrans. { apply maponpaths. rewrite <- tensor_id_id. rewrite <- inner_swap_inv. rewrite tensor_comp_id_l. apply idpath. } rewrite !assoc. apply maponpaths_2. etrans. { rewrite !assoc'. do 2 apply maponpaths. rewrite <- tensor_mor_left. refine (!_). apply inner_swap_hexagon. } rewrite tensor_mor_right. etrans. { apply maponpaths. rewrite !assoc. rewrite inner_swap_inv. rewrite id_left. apply idpath. } rewrite !assoc. etrans. { apply maponpaths_2. refine (!_). apply tensor_comp_id_r. } rewrite inner_swap_inv. rewrite tensor_id_id. apply 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.