@@ -15,6 +15,10 @@ class Applicative m => Monad (m : Type -> Type) where
15 (>>=) : m a -> (a -> m b) -> m b
15 (>>=) : m a -> (a -> m b) -> m b
17class (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
17class (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
18+ monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->
19+ mf <$> mx = mf >>= \f =>
18 monadLeftIdentity : (x : a) -> (f : a -> m b) -> return x >>= f = f x
22 monadLeftIdentity : (x : a) -> (f : a -> m b) -> return x >>= f = f x
19 monadRightIdentity : (mx : m a) -> mx >>= return = mx
23 monadRightIdentity : (mx : m a) -> mx >>= return = mx
20 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->
24 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->