Definition functor_to_eilenberg_moore_cat_preserves_initial {C' : category} (F : C' ⟶ C) (HF : preserves_initial F) (α : F ∙ m ⟹ functor_identity C' ∙ F) (p₁ : ∏ (x : C'), η m (F x) · α x = identity (functor_identity C (F x))) (p₂ : ∏ (x : C'), # m (α x) · α x = μ m (F x) · α x) : preserves_initial (functor_to_eilenberg_moore_cat m F α p₁ p₂). Proof. intros x Hx. use is_initial_eilenberg_moore_cat. - apply HF. exact Hx. - exact Hm. 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.