Lemma triangle_eq_swapping_of_tensor: triangle_eq swapping_of_tensor (monoidal_cat_unit M) (monoidal_cat_right_unitor M) (monoidal_cat_left_unitor M) associator_swapping_of_tensor. Proof. red. intros a b. cbn. set (H := monoidal_cat_triangle_eq M). unfold triangle_eq in H. etrans. 2: { apply cancel_precomposition. apply pathsinv0. apply H. } clear H. rewrite assoc. etrans. { apply pathsinv0. apply id_left. } apply cancel_postcomposition. apply pathsinv0. set (f := nat_z_iso_pointwise_z_iso (monoidal_cat_associator M)((b, monoidal_cat_unit M), a)). apply (z_iso_after_z_iso_inv f). Qed.
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.