Definition bincoproducts_eilenberg_moore : BinCoproducts (eilenberg_moore_cat m). Proof. intros x y. use make_BinCoproduct. - exact (bincoproduct_obj_eilenberg_moore x y). - exact (bincoproduct_eilenberg_moore_in1 x y). - exact (bincoproduct_eilenberg_moore_in2 x y). - use isBinCoproduct_eilenberg_moore. + exact Hm. + exact (pr2 (P (pr11 x) (pr11 y))). 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.