1      let Monad = ./../Monad/Type
 2  
 3  in    λ(s : Type)
 4      → λ(m : Type → Type)
 5      → λ(monad : Monad m)
 6      →   { lift =
 7              λ(a : Type) → (./transformer s).lift m monad a
 8          , eval =
 9              λ(a : Type) → ./eval s m monad a
10          , exec =
11              λ(a : Type) → ./exec s m monad a
12          , get =
13              ./get s m monad
14          , gets =
15              λ(a : Type) → ./gets s m monad a
16          , put =
17              λ(a : Type) → ./put s m monad
18          , modify =
19              λ(a : Type) → ./modify s m monad
20          }
21        ∧ ./monad s m monad