fold

{-
`fold` is the primitive function for consuming `List`s

If you treat the list `[ x, y, z ]` as `cons x (cons y (cons z nil))`, then a
`fold` just replaces each `cons` and `nil` with something else

Examples:

```
    ./fold
    Natural
    [ 2, 3, 5 ]
    Natural
    (λ(x : Natural) → λ(y : Natural) → x + y)
    0
=   10

    λ(nil : Natural)
→   ./fold
    Natural
    [ 2, 3, 5 ]
    Natural
    (λ(x : Natural) → λ(y : Natural) → x + y)
    nil
=   λ(nil : Natural) → 2 + 3 + 5 + nil

    λ(list : Type)
→   λ(cons : Natural → list → list)
→   λ(nil : list)
→   ./fold Natural [ 2, 3, 5 ] list cons nil
=   λ(list : Type)
→   λ(cons : Natural → list → list)
→   λ(nil : list)
→   cons 2 (cons 3 (cons 5 nil))
```
-}
    let fold
        :   ∀(a : Type)
          → List a
          → ∀(list : Type)
          → ∀(cons : a → list → list)
          → ∀(nil : list)
          → list
        = List/fold

in  fold