Definition functor_to_eilenberg_moore_cat_preserves_pullback {C' : category} (F : C' ⟶ C) (HF : preserves_pullback 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_pullback (functor_to_eilenberg_moore_cat m F α p₁ p₂). Proof. intros ? ? ? ? ? ? ? ? ? ? Hx. use isPullback_eilenberg_moore. - abstract (cbn ; rewrite <- !functor_comp ; apply maponpaths ; exact q). - use HF. + exact q. + 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.