Definition isPullback_eilenberg_moore_mor : w --> pb. Proof. use make_mor_eilenberg_moore. - use (PullbackArrow (make_Pullback _ H)). + exact (mor_of_eilenberg_moore_mor h). + exact (mor_of_eilenberg_moore_mor k). + exact (maponpaths (λ z, pr11 z) r). - use (MorphismsIntoPullbackEqual H). + abstract (rewrite !assoc' ; etrans ; [ apply maponpaths ; apply (PullbackArrow_PullbackPr1 (make_Pullback _ H)) | ] ; refine (!_) ; etrans ; [ apply maponpaths ; exact (pr21 π₁) | ] ; rewrite !assoc ; rewrite <- functor_comp ; etrans ; [ apply maponpaths_2 ; apply maponpaths ; apply (PullbackArrow_PullbackPr1 (make_Pullback _ H)) | ] ; exact (!(eq_of_eilenberg_moore_mor h))). + abstract (rewrite !assoc' ; etrans ; [ apply maponpaths ; apply (PullbackArrow_PullbackPr2 (make_Pullback _ H)) | ] ; refine (!_) ; etrans ; [ apply maponpaths ; exact (pr21 π₂) | ] ; rewrite !assoc ; rewrite <- functor_comp ; etrans ; [ apply maponpaths_2 ; apply maponpaths ; apply (PullbackArrow_PullbackPr2 (make_Pullback _ H)) | ] ; exact (!(eq_of_eilenberg_moore_mor k))). 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.