Definition monad_on_reflexive_coequalizer (HM : preserves_reflexive_coequalizer M) {X Y : hSet} {f g : SET ⟦ X , Y ⟧} {σ : SET ⟦ Y , X ⟧} (pf : ∏ (y : Y), f(σ y) = y) (pg : ∏ (y : Y), g(σ y) = y) : Coequalizer (#M f) (#M g). Proof. pose (C := pr11 (Coequalizers_HSET _ _ f g)). pose (π := CoequalizerArrow (Coequalizers_HSET _ _ f g)). simple refine ((M C ,, #M π) ,, _ ,, _). - abstract (refine (!(functor_comp M _ _) @ _ @ functor_comp M _ _) ; apply maponpaths ; exact (CoequalizerEqAr (Coequalizers_HSET _ _ f g))). - refine (HM X Y C f g σ _ _ π _ _ (pr22 (Coequalizers_HSET _ _ f g))). + abstract (use funextsec ; exact pf). + abstract (use funextsec ; exact pg). 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.