============

Consider the following list data type and its fold function in Agda[^1].

    data List (a : Set) : Set where
      Nil : List a
      Cons : a -> List a -> List a

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

The key word `Set` is a kind that classifies types. The function `fold` has two implicit type arguments, they correspond to the implicitly quantified type variables `a` and `p` in the type of `fold`. In Agda, implicit arguments can be supplied explicitly using braces (e.g. ``), sometimes they can be omitted.

The function `fold` is defined by structural recursion and it is terminating. Once `fold` is defined, we can use it to define terminating functions such as the following `map` and `sum`. This is similar to using the iterator to define terminating arithmetic functions in System **T** [@girard1989proofs §7].

    map : {a b : Set} -> (a -> b) -> List a -> List b
    map f l = fold Nil (\ 