fact: Definition disp_has_em (HB : bicat_has_em B) : UU := ∏ (m : mnd (total_bicat D)), let cone := pr1 (HB (pr1_of_mnd_total_bicat m)) in let ump := pr2 (HB (pr1_of_mnd_total_bicat m)) in ∑ (dob : D (pr1 cone)) (dmor : dob -->[ mor_of_mnd_mor (mor_of_em_cone (pr1_of_mnd_total_bicat m) cone) ] pr2 (ob_of_mnd m)) (dcell : dmor ;; pr2 (endo_of_mnd m) ==>[ mnd_mor_endo (mor_of_em_cone (pr1_of_mnd_total_bicat m) cone) ] id_disp _ ;; dmor), ∏ (q : em_cone m), pr21 q -->[ em_ump_1_mor _ ump (pr1_of_em_cone _ q) ] dob.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.DisplayedCats.Core UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.DispInvertibles UniMath.Bicategories.DisplayedBicats.Examples.EndoMap UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax UniMath.Bicategories.Limits.Final UniMath.Bicategories.Limits.Products UniMath.Bicategories.Limits.Pullbacks UniMath.Bicategories.Limits.EilenbergMooreObjects UniMath.Bicategories.Monads.Examples.MonadsInTotalBicat UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.PseudoFunctors.Examples.MonadInclusion