proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.ProductCategory UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.whiskering