Monad algebras

class MonadAlgebra (m : Type u → Type v) : Type (max (u + 1) v)

• monadAlg {α : Type u} : m α → α

class LawfulMonadAlgebra (m : Type u → Type v) [Monad m] [MonadAlgebra m] : Prop

• monadAlg_pure {α : Type u} (a : α) : monadAlg (pure a) = a
• monadAlg_bind {α β : Type u} (ma : m α) (mb : α → m β) : monadAlg (mb (monadAlg ma)) = monadAlg (ma >>= mb)