Definition bincoproduct_obj_eilenberg_moore_ob_mor (x y : eilenberg_moore_cat m) : m (bincoproduct_obj_eilenberg_moore_ob x y) --> bincoproduct_obj_eilenberg_moore_ob x y. Proof. use (BinCoproductArrow (make_BinCoproduct _ _ _ _ _ _ (Hm _ _ _ _ _ (pr2 (P (pr11 x) (pr11 y)))))). - exact (pr21 x · BinCoproductIn1 _). - exact (pr21 y · BinCoproductIn2 _). 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.