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