1      let Functor = ./../Functor/Type
 2  
 3  in    { map =
 4              λ(a : Type)
 5            → λ(b : Type)
 6            → λ(g : a → b)
 7            → λ(list : List a)
 8            → List/fold
 9              a
10              list
11              (List b)
12              (λ(x : a) → λ(xs : List b) → [ g x ] # xs)
13              ([] : List b)
14        }
15      : Functor List