Definition isBinCoproduct_eilenberg_moore_mor : sum --> w. Proof. use make_mor_eilenberg_moore. - exact (BinCoproductArrow copr (pr11 f) (pr11 g)). - use (BinCoproductArrowsEq _ _ _ (make_BinCoproduct _ _ _ _ _ _ (Hm _ _ _ _ _ H))) ; cbn. + abstract (rewrite !assoc ; rewrite <- functor_comp ; etrans ; [ apply maponpaths_2 ; exact (!(eq_of_eilenberg_moore_mor ι₁)) | ] ; rewrite !assoc' ; etrans ; [ apply maponpaths ; apply (BinCoproductIn1Commutes _ _ _ copr) | ] ; refine (!_) ; etrans ; [ apply maponpaths_2 ; apply maponpaths ; apply (BinCoproductIn1Commutes _ _ _ copr) | ] ; exact (!(eq_of_eilenberg_moore_mor f))). + abstract (rewrite !assoc ; rewrite <- functor_comp ; etrans ; [ apply maponpaths_2 ; exact (!(eq_of_eilenberg_moore_mor ι₂)) | ] ; rewrite !assoc' ; etrans ; [ apply maponpaths ; apply (BinCoproductIn2Commutes _ _ _ copr) | ] ; refine (!_) ; etrans ; [ apply maponpaths_2 ; apply maponpaths ; apply (BinCoproductIn2Commutes _ _ _ copr) | ] ; exact (!(eq_of_eilenberg_moore_mor 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.