proposition: Lemma psfunctor_to_lax_monoidal_functor_laws : monoidal_functor_associativity M N psfunctor_to_lax_monoidal_functor_functor μ × monoidal_functor_unitality M N psfunctor_to_lax_monoidal_functor_functor (pr1(psfunctor_id psF c0)) μ.
proof: Proof. split. * red. cbn. intros x y z. unfold rassociator_fun'. cbn. assert (Hyp := psfunctor_rassociator psF x y z). change ((id₂ (# psF z) ⋆⋆ psfunctor_comp psF x y • psfunctor_comp psF (x · y) z) • ## psF (rassociator x y z) = (rassociator (# psF x) (# psF y) (# psF z) • psfunctor_comp psF y z ⋆⋆ id₂ (# psF x)) • psfunctor_comp psF x (y · z)). rewrite hcomp_identity_right. rewrite hcomp_identity_left. exact Hyp. * red. cbn. intro x. split. -- change (lunitor (# psF x) = (id₂ (# psF x) ⋆⋆ psfunctor_id psF c0 • psfunctor_comp psF (id₁ c0) x) • ## psF (lunitor x)). rewrite hcomp_identity_right. apply psfunctor_lunitor. -- change (runitor (# psF x) = (psfunctor_id psF c0 ⋆⋆ id₂ (# psF x) • psfunctor_comp psF x (id₁ c0)) • ## psF (runitor x)). rewrite hcomp_identity_left. apply psfunctor_runitor. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Examples.BicategoryFromMonoidal UniMath.Bicategories.MonoidalCategories.MonoidalFromBicategory UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor