Proposition algebra_as_coequalizer_arr_eq : ℓ · algebra_as_coequalizer_arr = ρ · algebra_as_coequalizer_arr. Proof. unfold ℓ, ρ. unfold algebra_as_coequalizer_left_map. unfold algebra_as_coequalizer_right_map. use subtypePath. { intro. apply homset_property. } simpl. rewrite (functor_id M). etrans. { apply maponpaths_2. exact (id_left (μ M X)). } refine (monad_algebra_mu hX @ _). apply maponpaths_2. rewrite (functor_comp M). refine (_ @ assoc _ _ _). refine (!(id_right _) @ _). apply maponpaths. refine (!_). apply Monad_law2. 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.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Products. 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.Monads.Monads.