Definition inner_swap'' (x y z w : V) : V⟦(x ⊗ y) ⊗ (z ⊗ w), (x ⊗ z) ⊗ (y ⊗ w)⟧. Proof. refine (mon_lassociator _ _ _ · _). refine (x ⊗^{V}_{l} _ · _). - exact (sym_mon_braiding _ _ _ · mon_lassociator _ _ _). - exact (mon_rassociator x z (w ⊗ y) · (x ⊗ z) ⊗^{V}_{l} sym_mon_braiding _ w y). Defined.
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.