Definition monad_on_reflexive_coequalizer_2 (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(#M f)) (#M(#M g)). Proof. pose (C := pr11 (Coequalizers_HSET _ _ f g)). pose (π := CoequalizerArrow (Coequalizers_HSET _ _ f g)). simple refine ((M(M C) ,, #M(#M π)) ,, _ ,, _). - abstract (refine (!(functor_comp M _ _) @ _ @ functor_comp M _ _) ; apply maponpaths ; refine (!(functor_comp M _ _) @ _ @ functor_comp M _ _) ; apply maponpaths ; exact (CoequalizerEqAr (Coequalizers_HSET _ _ f g))). - simple refine (HM (M X) (M Y) (M C) (#M f) (#M g) (#M σ) _ _ (#M π) _ _ _). + abstract (refine (!(functor_comp M _ _) @ _ @ functor_id M _) ; apply maponpaths ; use funextsec ; exact pf). + abstract (refine (!(functor_comp M _ _) @ _ @ functor_id M _) ; apply maponpaths ; use funextsec ; exact pg). + 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.