Definition swapping_of_lax_monoidal_functor: lax_monoidal_functor Mon Mon' -> lax_monoidal_functor (swapping_of_monoidal_cat Mon) (swapping_of_monoidal_cat Mon'). Proof. intro lmF. induction lmF as [F [ϵ [μ [Hass Hunit]]]]. use make_lax_monoidal_functor. - exact F. - exact ϵ. - exact (pre_whisker binswap_pair_functor μ). - apply (swapping_of_lax_monoidal_functor_assoc (F,, (ϵ,, (μ,, (Hass,, Hunit))))). - abstract ( red; intro x; induction (Hunit x) as [Hunit1 Hunit2]; split; assumption ). Defined.
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.