1      let Monad = ./../Monad/Type
 2  
 3  in  let concatMap =
 4              λ(a : Type)
 5            → λ(b : Type)
 6            → λ(f : a → List b)
 7            → λ(xs : List a)
 8            → List/build
 9              b
10              (   λ(list : Type)
11                → λ(cons : b → list → list)
12                → List/fold a xs list (λ(x : a) → List/fold b (f x) list cons)
13              )
14  
15  in      ./applicative
16        ∧ { bind =
17                λ(a : Type)
18              → λ(b : Type)
19              → λ(fa : List a)
20              → λ(k : a → List b)
21              → concatMap a b k fa
22          }
23      : Monad List