Definition MonadAlg_disp_ob_mor {C : category} (T : Monad C) : disp_cat_ob_mor C. Proof. use make_disp_cat_ob_mor. - intro X. exact (∑ (α : (T X) --> X), Algebra_laws _ (make_Algebra_data T X α)). - intros X Y αX αY f. set (X' := make_Algebra_data T X (pr1 αX),, pr2 αX : Algebra T). set (Y' := make_Algebra_data T Y (pr1 αY),, pr2 αY : Algebra T). exact (is_Algebra_mor T (X:=X') (Y:=Y') f). 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.