1      let Applicative = ./../Applicative/Type
2  
3  in    λ(r : Type)
4      → λ(m : Type → Type)
5      → λ(applicative : Applicative m)
6      → λ(a : Type)
7      → λ(f : r → a)
8      → λ(env : r)
9      → applicative.pure a (f env)