fact: Definition op2_bicat_has_em_ump_2_help : αcell • (_ ◃ cell_of_em_comnd_cone m e) • lassociator _ _ _ = (_ ◃ cell_of_em_comnd_cone m e) • lassociator _ _ _ • (αcell ▹ endo_of_mnd m).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Examples.OpCellBicat UniMath.Bicategories.Limits.Final UniMath.Bicategories.Limits.Products UniMath.Bicategories.Limits.Pullbacks UniMath.Bicategories.Limits.CommaObjects UniMath.Bicategories.Limits.EilenbergMooreObjects UniMath.Bicategories.Limits.EilenbergMooreComonad UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.PseudoFunctors.Examples.MonadInclusion