Definition MonadAlg_disp {C : category} (T : Monad C) : disp_cat C. Proof. use tpair. - exact (MonadAlg_disp_data T). - abstract ( repeat split; intros; try (apply homset_property); apply isasetaprop; apply homset_property ). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Monads.MonadAlgebras. Require Import UniMath.CategoryTheory.Monads.Comonads. Require Import UniMath.CategoryTheory.Monads.ComonadCoalgebras. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total.