Proposition monad_reflexive_coequalizer_algebra_laws : monad_algebra_laws M monad_reflexive_coequalizer_algebra_mor. Proof. split. - use (CoequalizerOutsEq Coeq). rewrite id_right. unfold monad_reflexive_coequalizer_algebra_mor. rewrite !assoc. etrans. { apply maponpaths_2. exact (nat_trans_ax (η M) _ _ (CoequalizerArrow Coeq)). } rewrite !assoc'. etrans. { apply maponpaths. apply (CoequalizerCommutes (monad_on_reflexive_coequalizer _ _ _)). } rewrite !assoc. rewrite monad_algebra_unit. apply id_left. - use (CoequalizerOutsEq (monad_on_reflexive_coequalizer_2 HM pf pg)). unfold monad_reflexive_coequalizer_algebra_mor. rewrite !assoc. etrans. { apply maponpaths_2. apply (nat_trans_ax (μ M)). } rewrite !assoc'. etrans. { apply maponpaths. apply (CoequalizerCommutes (monad_on_reflexive_coequalizer _ _ _)). } rewrite !assoc. rewrite monad_algebra_mu. refine (!_). etrans. { apply maponpaths_2. refine (!(functor_comp _ _ _) @ _). apply maponpaths. apply (CoequalizerCommutes (monad_on_reflexive_coequalizer _ _ _)). } rewrite functor_comp. rewrite !assoc'. apply maponpaths. apply (CoequalizerCommutes (monad_on_reflexive_coequalizer _ _ _)). Qed.
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.