Definition binary_coprod_algebra_arrow : binary_coprod_algebra_ob --> Z. Proof. use CoequalizerOut. - exact binary_coprod_algebra_arrow_ob. - use BinCoproductArrowsEq. + abstract (rewrite !assoc ; unfold l, binary_coprod_algebra_left_map ; unfold r, binary_coprod_algebra_right_map ; unfold binary_coprod_algebra_arrow_ob ; rewrite !BinCoproductOfArrowsIn1 ; rewrite !assoc' ; rewrite BinCoproductIn1Commutes ; rewrite !assoc ; apply maponpaths_2 ; exact (!(nat_trans_ax (monad_free_alg_counit M) _ _ _))). + abstract (rewrite !assoc ; unfold l, binary_coprod_algebra_left_map ; unfold r, binary_coprod_algebra_right_map ; unfold binary_coprod_algebra_arrow_ob ; rewrite !BinCoproductOfArrowsIn2 ; rewrite !assoc' ; rewrite BinCoproductIn2Commutes ; rewrite !assoc ; apply maponpaths_2 ; exact (!(nat_trans_ax (monad_free_alg_counit M) _ _ _))). 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.