@@ -14,6 +14,12 @@ infixl 5 >>=
1414class Applicative m => Monad (m : Type -> Type) where
1515 (>>=) : m a -> (a -> m b) -> m b
1616
17+class Monad m => VerifiedMonad (m : Type -> Type) where
18+ total lIdentity : (f : a -> m b) -> (x : a) -> return x >>= f = f x
19+ total rIdentity : (ma : m a) -> ma >>= return = ma
20+ total associativity : (ma : m a) -> (f : a -> m b) -> (g : b -> m c) ->
21+ (ma >>= f) >>= g = ma >>= (\x => f x >>= g)
22+
1723instance Monad id where
1824 a >>= f = f a
1925