Definition binary_coprod_algebra : BinCoproduct alg_X alg_Y. Proof. use make_BinCoproduct. - exact binary_coprod_algebra_ob. - exact binary_coprod_algebra_in1. - exact binary_coprod_algebra_in2. - intros Z φ₁ φ₂. use iscontraprop1. + exact (binary_coprod_algebra_arrow_unique φ₁ φ₂). + simple refine (_ ,, _ ,, _). * exact (binary_coprod_algebra_arrow φ₁ φ₂). * exact (binary_coprod_algebra_arrow_in1 φ₁ φ₂). * exact (binary_coprod_algebra_arrow_in2 φ₁ φ₂). Defined.
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.Adjunctions.Core. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.AlgebraStructures. Require Import UniMath.CategoryTheory.Monads.Monads.