proposition: Lemma MonadAlg_disp_is_Algebra {C : category} (T : Monad C) : MonadAlg_tot T = MonadAlg T.
proof: Proof. apply catiso_to_category_path. use tpair. - exact (MonadAlg_disp_Algebra_functor T). - split. * intros a b. use isweq_iso. + exact (idfun _). + intros. apply idpath. + intros. apply idpath. * use isweq_iso. + intros [[x α] laws]. use tpair. -- exact x. -- exact (α,, laws). + intro. apply idpath. + intro. apply idpath. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monads.MonadAlgebras UniMath.CategoryTheory.Monads.Comonads UniMath.CategoryTheory.Monads.ComonadCoalgebras UniMath.CategoryTheory.catiso UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total