LIST

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

Introduction

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

Elimination

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