Definition eilenberg_moore_cat_ump_1 : em_ump_1 m eilenberg_moore_cat_cone. Proof. intro q. use make_em_cone_mor. - use functor_to_eilenberg_moore_cat. + exact (mor_of_mnd_mor (mor_of_em_cone _ q)). + exact (mnd_mor_endo (mor_of_em_cone _ q)). + abstract (intro x ; pose (nat_trans_eq_pointwise (mnd_mor_unit (mor_of_em_cone _ q)) x) as p ; cbn in p ; rewrite (functor_id (mor_of_mnd_mor (mor_of_em_cone m q))) in p ; rewrite !id_left in p ; exact (!p)). + abstract (intro x ; pose (nat_trans_eq_pointwise (mnd_mor_mu (mor_of_em_cone _ q)) x) as p ; cbn in p ; rewrite (functor_id (mor_of_mnd_mor (mor_of_em_cone m q))) in p ; rewrite !id_left, !id_right in p ; exact p). - use make_invertible_2cell. + use make_mnd_cell. * apply functor_to_eilenberg_moore_cat_pr. * abstract (use nat_trans_eq ; [ apply homset_property | ] ; intro x ; cbn ; rewrite (functor_id (endo_of_mnd m)) ; rewrite !id_left, !id_right ; apply idpath). + use is_invertible_mnd_2cell. use is_nat_z_iso_to_is_invertible_2cell. apply functor_to_eilenberg_moore_cat_pr_is_nat_z_iso. Defined.
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.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.Categories.Dialgebras. Require Import UniMath.CategoryTheory.Categories.CatIsoInserter. Require Import UniMath.CategoryTheory.Categories.EilenbergMoore. Require Import UniMath.CategoryTheory.Subcategory.Core. Require Import UniMath.CategoryTheory.Subcategory.Full. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.IsoCommaCategory. Require Import UniMath.CategoryTheory.CommaCategories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Reindexing. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Limits.Final. Require Import UniMath.Bicategories.Limits.Products. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.CommaObjects. Require Import UniMath.Bicategories.Limits.Inserters. Require Import UniMath.Bicategories.Limits.Equifiers. Require Import UniMath.Bicategories.Limits.IsoInserters. Require Import UniMath.Bicategories.Limits.EilenbergMooreObjects. Require Import UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax. Require Import UniMath.Bicategories.Monads.Examples.MonadsInBicatOfUnivCats.