Definition Pullbacks_eilenberg_moore : Pullbacks (eilenberg_moore_cat m). Proof. intros x y z f g. use make_Pullback. - exact (pullbacks_eilenberg_moore_ob f g). - exact (pullbacks_eilenberg_moore_pr1 f g). - exact (pullbacks_eilenberg_moore_pr2 f g). - exact (pullbacks_eilenberg_moore_eq f g). - refine (isPullback_eilenberg_moore _ _ _). exact (pr22 (PB _ _ _ (pr11 f) (pr11 g))). 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.