Definition cmonoidal_from_noncurried_functor (M N : ob UMONCAT) : UMONCAT ⟦ M, N ⟧ → LaxMonoidalFunctorCat (pr1 (cmonoidal_to_noncurriedmonoidal M)) (pr1 (cmonoidal_to_noncurriedmonoidal N)). Proof. intro F. use tpair. - exists (pr1 F). split. + use tpair. * intro ; apply (pr1 (pr112 F)). * intros [x1 x2] [y1 y2] [f g]. etrans. { apply maponpaths_2, (! tensor_on_hom_eq N _ _). } refine (! pr21 (pr112 F) x1 y1 x2 y2 f g @ _). simpl. do 2 apply maponpaths. apply tensor_on_hom_eq. + apply (pr2 (pr112 F)). - repeat split. + abstract ( intro x ; refine (! (pr11 (pr212 F) x) @ _) ; do 2 apply maponpaths_2 ; apply (tensor_on_hom_eq N)). + abstract ( intro x ; refine (! (pr21 (pr212 F) x) @ _) ; do 2 apply maponpaths_2 ; apply (tensor_on_hom_eq N)). + intros x y z. apply TODO. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorCategory. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.EquivalenceWhiskeredNonCurriedMonoidalCategories. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesReordered. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.CurriedMonoidalCategories. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.AssociatorUnitorsLayer. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.FinalLayer. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.CurriedMonoidalCategories. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.AssociatorUnitorsLayer. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.FinalLayer. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.EquivalenceMonCatCurried. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.EquivalenceWhiskeredCurried.