Definition eilenberg_moore_cat_ump_2 : em_ump_2 m eilenberg_moore_cat_cone. Proof. intros C' F₁ F₂ α. use iscontraprop1. - abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply cellset_property | ] ; use nat_trans_eq ; [ apply homset_property | ] ; intro x ; pose (nat_trans_eq_pointwise (maponpaths pr1 (pr2 φ₁)) x) as p₁ ; pose (nat_trans_eq_pointwise (maponpaths pr1 (pr2 φ₂)) x) as p₂ ; use eq_mor_eilenberg_moore ; exact (p₁ @ (!p₂))). - simple refine (_ ,, _). + use nat_trans_to_eilenberg_moore_cat. * exact (cell_of_mnd_cell α). * abstract (intro x ; pose (nat_trans_eq_pointwise (mnd_cell_endo α) x) as p ; simpl in p ; rewrite !id_left, !id_right in p ; exact p). + abstract (use eq_mnd_cell ; use nat_trans_eq ; [ apply homset_property | ] ; intro x ; apply idpath). 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.