1      let Applicative = ./../Applicative/Type
 2  
 3  in  let fold = (./foldable).fold
 4  
 5  in  let map = (./functor).map
 6  
 7  in      ./functor
 8        ∧ { pure =
 9              λ(a : Type) → λ(x : a) → [ x ]
10          , ap =
11                λ(a : Type)
12              → λ(b : Type)
13              → λ(g : List (a → b))
14              → λ(fa : List a)
15              → fold
16                (a → b)
17                g
18                (List b)
19                (λ(k : a → b) → λ(xs : List b) → map a b k fa # xs)
20                ([] : List b)
21          }
22      : Applicative List