Lemma swapping_of_lax_monoidal_functor_assoc (lmF: lax_monoidal_functor Mon Mon'): monoidal_functor_associativity (swapping_of_monoidal_cat Mon) (swapping_of_monoidal_cat Mon') lmF (pre_whisker binswap_pair_functor (lax_monoidal_functor_μ lmF)). Proof. induction lmF as [F [ϵ [μ [Hass Hunit]]]]. red. intros x y z. set (Hass_inst := Hass z y x). apply pathsinv0. rewrite <- assoc. cbn. set (f := nat_z_iso_pointwise_z_iso (monoidal_cat_associator Mon') ((F z, F y), F x)). apply (z_iso_inv_on_right _ _ _ f). transparent assert (is : (is_z_isomorphism (# F (monoidal_cat_associator Mon ((z, y), x))))). { apply functor_on_is_z_isomorphism. apply monoidal_cat_associator. } set (Hass_inst' := z_iso_inv_on_left _ _ _ _ (_,, is) _ (! Hass_inst)). etrans. { exact Hass_inst'. } clear Hass_inst Hass_inst'. do 2 rewrite assoc. apply cancel_precomposition. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.whiskering.