Definition monad_reflexive_coequalizer_ump_mor : monad_reflexive_coequalizer_ob --> AW. Proof. simple refine (_ ,, _). - exact (CoequalizerOut Coeq _ l p). - abstract (use (CoequalizerOutsEq (monad_on_reflexive_coequalizer HM pf pg)) ; refine (assoc _ monad_reflexive_coequalizer_algebra_mor _ @ _) ; unfold monad_reflexive_coequalizer_algebra_mor ; rewrite !assoc ; rewrite (CoequalizerCommutes (monad_on_reflexive_coequalizer HM pf pg)) ; rewrite !assoc' ; rewrite (CoequalizerCommutes Coeq) ; refine (hl @ _) ; rewrite !assoc ; refine (maponpaths (λ z, z · _) (!_)) ; refine (!(functor_comp M _ _) @ _) ; apply maponpaths ; apply (CoequalizerCommutes Coeq)). 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.