Definition swapping_of_strong_monoidal_functor: strong_monoidal_functor Mon Mon' -> strong_monoidal_functor (swapping_of_monoidal_cat Mon) (swapping_of_monoidal_cat Mon'). Proof. intro smF. induction smF as [lmF [Hϵ Hμ]]. apply (tpair _ (swapping_of_lax_monoidal_functor lmF)). split. - exact Hϵ. - exact (pre_whisker_on_nat_z_iso binswap_pair_functor (lax_monoidal_functor_μ lmF) Hμ). 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.