Definition MonadAlg_disp_Algebra_functor {C : category} (T : Monad C) : MonadAlg_tot T ⟶ (MonadAlg T). Proof. use make_functor. - use make_functor_data. * intro X. exact (Algebra_from_MonadAlg_disp (pr2 X)). * intros. exact (Algebra_mor_from_Algebra_mor_disp (pr2 a) (pr2 b) (pr2 X)). - abstract ( split; [intro|intros a b c f g]; (apply subtypePath; [intro; apply homset_property|]; reflexivity) ). 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.