Lemma pentagon_eq_swapping_of_tensor: pentagon_eq swapping_of_tensor associator_swapping_of_tensor. Proof. red. intros a b c d. cbn. set (H := monoidal_cat_pentagon_eq M). unfold pentagon_eq in H. set (f := nat_z_iso_pointwise_z_iso (monoidal_cat_associator M) ((d, c), monoidal_cat_tensor M (b, a))). apply (z_iso_inv_on_right _ _ _ f). apply pathsinv0. set (f' := nat_z_iso_pointwise_z_iso (monoidal_cat_associator M) ((monoidal_cat_tensor M (d, c), b), a)). apply (inv_z_iso_unique' _ _ _ f'). unfold precomp_with. rewrite assoc. etrans. { apply cancel_postcomposition. apply H. } clear H. repeat rewrite assoc. etrans. { do 2 apply cancel_postcomposition. rewrite <- assoc. apply cancel_precomposition. apply pathsinv0. apply (functor_comp (functor_fix_fst_arg _ _ _ (monoidal_cat_tensor M) d)). } etrans. { do 2 apply cancel_postcomposition. apply cancel_precomposition. apply maponpaths. apply (z_iso_inv_after_z_iso (nat_z_iso_pointwise_z_iso (monoidal_cat_associator M) ((c, b), a))). } rewrite functor_id. rewrite id_right. etrans. { apply cancel_postcomposition. rewrite <- assoc. apply cancel_precomposition. apply (z_iso_inv_after_z_iso (nat_z_iso_pointwise_z_iso (monoidal_cat_associator M) ((d, monoidal_cat_tensor M (c, b)), a))). } rewrite id_right. etrans. apply pathsinv0. apply (functor_comp (functor_fix_snd_arg _ _ _ (monoidal_cat_tensor M) a)). etrans. { apply maponpaths. apply (z_iso_inv_after_z_iso (nat_z_iso_pointwise_z_iso (monoidal_cat_associator M) ((d, c), b))). } cbn. unfold functor_fix_snd_arg_mor. use functor_id. 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.