Definition wmonfunctor_to_cmontensorunitfunctor : wmonfunctor -> functor_tensor_unit MC MD F. Proof. intro wmf. split. - exists (pr11 wmf). intros x1 x2 y1 y2 f g. assert (p0 : #F (tensor_on_hom MC _ _ _ _ f g) = #F (tensor_on_hom MC _ _ _ _ f (identity y1)) · #F (tensor_on_hom MC _ _ _ _ (identity x2) g)). { etrans. 2: { apply functor_comp. } apply maponpaths. refine (_ @ tensor_comp _ _ _ _ _ _ _ f (identity x2) (identity y1) g). etrans. 2: { apply maponpaths_2 ; apply (! id_right _). } apply maponpaths ; apply (! id_left _). } etrans. { apply maponpaths ; apply p0. } etrans. { apply assoc. } etrans. { apply maponpaths_2 ; apply (! pr122 wmf x1 x2 y1 f). } etrans. { apply assoc'. } etrans. { apply maponpaths ; apply (! pr12 wmf x2 y1 y2 g). } etrans. { apply assoc. } apply maponpaths_2. etrans. 2: { do 2 apply maponpaths. apply id_left. } etrans. 2: { apply maponpaths_2. apply maponpaths. apply id_right. } etrans. 2: { apply maponpaths. apply (! functor_comp _ _ _). } etrans. 2: { apply maponpaths_2. apply (! functor_comp _ _ _). } refine (_ @ ! tensor_comp _ _ _ _ _ _ _ _ _ _ _). etrans. 2: { apply maponpaths. apply maponpaths_2. apply (! functor_id _ _). } apply maponpaths_2. etrans. 2: { apply maponpaths. apply (! functor_id _ _). } apply idpath. - exact (pr21 wmf). 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.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesReordered. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.CurriedMonoidalCategories. Import BifunctorNotations.