a r -> Cons (f a) r) l
    sum : List Nat -> Nat
    sum l = fold Z (\ x r -> add x r) l

When defining the `map` function, if the input list `l` is empty, then we just return `Nil`, so the first argument for `fold` is `Nil`. If the input list `l` is of the form `Cons a as`, then we want to return `Cons (f a) (map f as)`, so the second argument for `fold` is ` a r -> Cons (f a) r`, where `r` represents the result of the recursive call `map f as`. The function `sum` is defined similarly.

We can generalize the type of `fold` to obtain the following induction principle for list.

    ind : {a : Set} {p : List a -> Set} -> p Nil ->
              ((x : a) -> {xs : List a} -> p xs -> p (Cons x xs)) -> (l : List a) -> p l
    ind {a} {p} base step Nil = base
    ind {a} {p} base step (Cons x xs) = step x {xs} (ind {a} {p} base step xs)

Ignoring the implicit arguments, the definition of `ind` is the same as 