proposition: Proposition algebra_as_coequalizer_arr_eq : ℓ · algebra_as_coequalizer_arr = ρ · algebra_as_coequalizer_arr.
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Categories.HSET.All UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Preservation UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits UniMath.CategoryTheory.Monads.Monads