Definition mor_of_pullbacks_eilenberg_moore_ob : m ob_of_pullbacks_eilenberg_moore_ob --> ob_of_pullbacks_eilenberg_moore_ob. Proof. use PullbackArrow. - exact (# m (PullbackPr1 (PB _ _ _ (pr11 f) (pr11 g))) · pr21 x). - exact (# m (PullbackPr2 (PB _ _ _ (pr11 f) (pr11 g))) · pr21 y). - abstract (rewrite !assoc' ; refine (maponpaths (λ z, _ · z) (pr21 f) @ _) ; refine (_ @ !(maponpaths (λ z, _ · z) (pr21 g))) ; rewrite !assoc ; rewrite <- !functor_comp ; apply maponpaths_2 ; apply maponpaths ; apply PullbackSqrCommutes). 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.