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. 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.
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.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.Core.Examples.BicategoryFromMonoidal. Require Import UniMath.Bicategories.MonoidalCategories.MonoidalFromBicategory. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Import Bicat.Notations.