Lemma has_homsets_MonadAlg : has_homsets MonadAlg_precat. Proof. intros X Y. apply (isofhleveltotal2 2). - apply homset_property. - intro f. apply isasetaprop. apply homset_property. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Monads.Derivative.