1      let Traversable = ./../Traversable/Type
 2  
 3  in  let Applicative = ./../Applicative/Type
 4  
 5  in  let liftA2 = ./../Applicative/liftA2
 6  
 7  in  let fold = (./foldable).fold
 8  
 9  in      ./foldable
10        ∧ ./functor
11        ∧ { traverse =
12                λ(f : Type → Type)
13              → λ(applicative : Applicative f)
14              → λ(a : Type)
15              → λ(b : Type)
16              → λ(g : a → f b)
17              → λ(ts : List a)
18              →     let liftCons =
19                          liftA2
20                          f
21                          applicative
22                          b
23                          (List b)
24                          (List b)
25                          (λ(x : b) → λ(xs : List b) → [ x ] # xs)
26                
27                in  fold
28                    a
29                    ts
30                    (f (List b))
31                    (λ(x : a) → λ(y : f (List b)) → liftCons (g x) y)
32                    (applicative.pure (List b) ([] : List b))
33          }
34      : Traversable List