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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.Examples.EndoMap. Require Import UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax. Require Import UniMath.Bicategories.Limits.Final. Require Import UniMath.Bicategories.Limits.Products. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.EilenbergMooreObjects. Require Import UniMath.Bicategories.Monads.Examples.MonadsInTotalBicat. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Examples.MonadInclusion.