The data type of over a given set can be represented as the initial algebra of the functor . Denote . The constructor functions and are defined by and , so .

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

In type theory type could be expressed as


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

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


Induction principle allows you to prove general predicate on from predicates on constructors and .

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