Definition is_initial_eilenberg_moore_cat (I : eilenberg_moore_cat m) (HI : isInitial _ (pr11 I)) (Hm : preserves_initial m) : isInitial (eilenberg_moore_cat m) I. Proof. use make_isInitial. intro x. use make_iscontr. - use make_mor_eilenberg_moore. + apply (InitialArrow (make_Initial _ HI)). + apply (@InitialArrowEq _ (make_Initial _ (Hm _ HI))). - abstract (intro f ; use eq_mor_eilenberg_moore ; apply (@InitialArrowEq _ (make_Initial _ HI))). 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.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.Dialgebras. Require Import UniMath.CategoryTheory.Categories.EilenbergMoore. Require Import UniMath.CategoryTheory.Subcategory.Core. Require Import UniMath.CategoryTheory.Subcategory.Full. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Preservation.