1      let ReaderT = ./Type
 2  
 3  in  let Monad = ./../Monad/Type
 4  
 5  in  let extractApplicative = ./../Monad/extractApplicative
 6  
 7  in    λ(r : Type)
 8      → λ(m : Type → Type)
 9      → λ(monad : Monad m)
10      →   { lift =
11              λ(a : Type) → (./transformer r).lift m monad a
12          , ask =
13              ./ask r m (extractApplicative m monad)
14          , asks =
15              λ(a : Type) → ./asks r m (extractApplicative m monad) a
16          , local =
17                λ(a : Type)
18              → λ(f : r → r)
19              → λ(reader : ReaderT r m a)
20              → ./local r m a f reader
21          }
22        ∧ ./monad r m monad