Definition monad_reflexive_coequalizer : Coequalizer Af Ag. Proof. use make_Coequalizer. - exact monad_reflexive_coequalizer_ob. - exact monad_reflexive_coequalizer_arrow. - exact monad_reflexive_coequalizer_arrow_eq. - intros W h p. use iscontraprop1. + exact (monad_reflexive_coequalizer_ump_unique (pr2 W) (pr2 h)). + simple refine (_ ,, _). * apply (monad_reflexive_coequalizer_ump_mor (pr2 W) (pr2 h)). exact (maponpaths pr1 p). * apply monad_reflexive_coequalizer_ump_commutes. 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.