LIST

The data type of list over a given set A can be represented as the initial algebra (μ L_A, in) of the functor L_A(X) = 1 + (A × X). Denote μ L_A = 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

Constructors

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

Eliminators

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