Definition monoidal_functor_to_psfunctor_map_data: psfunctor_data M_as_bicat N_as_bicat. Proof. use make_psfunctor_data. - cbn. exact (fun x => x). - intros a b. cbn. exact (functor_on_objects smF). - intros a b f g. cbn. exact (functor_on_morphisms smF). - intros a. cbn. exact (lax_monoidal_functor_ϵ smF). - intros a b c f g. cbn. apply (lax_monoidal_functor_μ smF (f,g)). 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.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.