Definition functor_to_eilenberg_moore_cat_preserves_bincoproduct {C' : category} (F : C' ⟶ C) (HF : preserves_bincoproduct 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_bincoproduct (functor_to_eilenberg_moore_cat m F α p₁ p₂). Proof. intros x y p π₁ π₂ Hx. use isBinCoproduct_eilenberg_moore. - exact Hm. - apply HF. exact Hx. 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.