The data type of list over a given set A can be represented as the initial algebra (μ LA, in) of the functor LA(X) = 1 + (A × X). Denote μ LA = List(A). The constructor functions nil: 1 → List(A) and cons: A × List(A) → List(A) are defined by nil = in β—¦ inl and cons = in β—¦ inr, so in = [nil,cons].

In type theory $List$ type could be expressed as $$ List(A) := W_{(x:1+A)},\ rec_{1+A}(A,U,0,λa.𝟏,x). $$

def List-ctor (A: U) := maybe-rec A U 𝟎 (λ (a : A), 𝟏) def List (A: U) := W (x : Maybe A), List-ctor A x


You can create zero list with nil and append an element to the head of the list with cons.

def nil (A: U) : List A def cons (A: U) (x : A) (xs: List A) : List A

Induction Principle

Induction principle allows you to prove general predicate on List (C n) from predicates on constructors (C nil) and (C cons).

def List-ind (A: U) (C: List A -> U) (z: C (nil A)) (s: Ξ  (x: A) (xs: List A), C xs -> C (cons A x xs)) : Ξ  (n: List A), C n


def List-rec (A: U) (C : U) (z : C) (s : A β†’ List A β†’ C β†’ C) : List A β†’ C def List-iter (A: U) (C : U) (z : C) (s : A β†’ C β†’ C) : List A β†’ C def List-case (A: U) (C : U) (z : C) (s : A β†’ C) : List A β†’ C