1      let Reader = ./Type
 2  
 3  in  let Applicative = ./../Applicative/Type
 4  
 5  in    λ(r : Type)
 6      →     ./functor r
 7          ∧ { pure =
 8                λ(a : Type) → λ(x : a) → λ(env : r) → x
 9            , ap =
10                  λ(a : Type)
11                → λ(b : Type)
12                → λ(g : Reader r (a → b))
13                → λ(fa : Reader r a)
14                → λ(env : r)
15                → g env (fa env)
16            }
17        : Applicative (Reader r)