Definition make_mnd_enriched_cats {C : univalent_category} (E : enrichment C V) (M : Monad C) (EM : monad_enrichment E M) : mnd (bicat_of_enriched_cats V). Proof. use make_mnd_total_bicat. - apply disp_2cell_isapprop_enriched_cats. - exact (Monad_to_mnd_bicat_of_univ_cats M). - use make_disp_mnd ; cbn. + exact E. + exact EM. + exact (unit_of_monad_enrichment EM). + exact (mu_of_monad_enrichment EM). 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.Core.Univalence. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentMonad. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax. Require Import UniMath.Bicategories.DisplayedBicats.Examples.EnrichedCats. Require Import UniMath.Bicategories.Monads.Examples.MonadsInBicatOfUnivCats. Require Import UniMath.Bicategories.Monads.Examples.MonadsInTotalBicat.