Definition associator_swapping_of_tensor: associator swapping_of_tensor. Proof. set (α := monoidal_cat_associator M). set (α' := nat_z_iso_to_trans_inv α). red. set (trafo := (pre_whisker reverse_three_args α'): (assoc_left swapping_of_tensor) ⟹ (assoc_right swapping_of_tensor)). assert (tisziso: is_nat_z_iso trafo). { red. intro c. set (aux := pr2 (nat_z_iso_inv α)). apply (pre_whisker_on_nat_z_iso reverse_three_args α' aux). } exact (trafo,, tisziso). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.whiskering.