Type Theory

x :≡ y means that x is a new name and that for now on, whenever one reads x, one may replace x by y.

x ≡ y means that whenever one read x, one may replace x by y as it was already introduced before using :≡.

🞎 is a "hole" to be completed.

… means that something is implicit and correctly typed.

Why

We want to express the fact that there is a way to start from here and get to there.

For instance, given a number, say 0, there is a unique string representation "0". So, we say: string(0) :≡ "0".

More over, if we call our numbers ℕ, then for all n : ℕ, we have string(n) : String.

We may see string as the name of a path, i.e. a way, to get from ℕ to String.

Formation

X, Y : Type
X → Y : Type

Introduction

x : X, y is a formula such that y(x) : Y
λx.y : X → Y
x ↦ y :≡ λx.y

Elimination

f : X → Y
x : X
f(x) : Y :≡ (λx.y)(x)

Why

We want to express the fact that there is a way to start from here and get to there ; but the place we end up depends on where we start.

For instance, we might want to start from ℕ and end up in String or ℕ depending on where we started from.

For instance, if n is even, then f(n) :≡ n and if n is odd, then f(n) :≡ string(n).

Formation

Y : X → Type
Π(x:X),Y(x) : Type

Introduction

Y : X → Type
x : X
y formula such that y(x) : Y(x)
λx.y : Π(x:X),Y(x)

Elimination

f : Π(x:X),Y(x)
x : X
f(x) : Y(x) :≡ (λx.y)(x)

Standard function composition.

∘ : (A → B) (B → C) → A → C :≡ f g a ↦ g(f(a))

We want to define "pipelines" of transformations that can be read left to right.

▸ : (A → B) (B → C) → A → C :≡ f g ↦ g ∘ f
a ▸ f ▸ g :≡ ▸(f g)(a)

Why

Given two types of instances X and Y, we might want to consider both instances at the same time.

For instance, we might want to speak about the pair Capital and Country like Paris and France at the same time.

Formation

X, Y : Type
X × Y : Type

Introduction

< , > : X Y → X × Y

Elimination

f : X → Y → Z
φ : X × Y → Z :≡ <x, y> ↦ f(x)(y)

C : X × Y → Type
f : Π(x:X,y:Y),C(<x,y>)
φ : Π(p:X×Y),C(p) :≡ <x, y> ↦ f(x)(y)

Why

We want instances of some type such that they represent a pair of instances where the second instance type depends on the first instance.

For instance, we might want to speak about pairs such that the second components is a string if the firt component is an even number.

Formation

X : Type
Y : X → Type
Σ(x:X),Y(x) : Type

Introduction

< , > : x:X Y(x) → Σ(x:X),Y(x)

Elimination

f : Π(x:X),Y(x) → Z
φ : Σ(x:X),Y(x) → Z :≡ <x, y> ↦ f(x)(y)

C : Π(x:X),Y(x) → Type
f : Π(x:X) Π(y:Y(x)) C(<x,y>)
φ : Π(p:Π(x:X),Y(x)),C(p) :≡ <x, y> ↦ f(x)(y)

Magma :≡ Σ(A:Type)(A → A → A)

PointedMagma :≡ Σ(A:Type)(A → A → A) × A

Why

Given two types X and Y, we might want to consider an instance that may be of one type or the other.

For instance, we might want to speak about a Capital or a Country like Paris or France.

Formation

X, Y : Type
X + Y : Type

Introduction

left : X → X + Y
right : Y → X + Y

Elimination

elim : (f : X → Z) (g : Y → Z) → X + Y → Z :≡
  left(x) ↦ f(x)
  right(y) ↦ g(y)

Target :≡ X + Y → Type
Left : Target → Type :≡ C ↦ Π(x:X),C((left(x)))
Right : Target → Type :≡ C ↦ Π(y:Y),C((right(y)))
ind : C:Target Left(C) Right(C) → Π(p:X+Y),C(p) :≡
  left(x) ↦ f(x)
  right(y) ↦ g(y)

Why

We want to be able to count things.

Formation

ℕ : Type

Introduction

0 : ℕ
succ : ℕ → ℕ
n+1 :≡ succ(n)

Elimination

T  : Type
elim : t:T → (next : ℕ T → T) → ℕ → T :≡
  0 ↦ t
  n+1 ↦ next n f(n)

P : ℕ → Type
Init :≡ P(0)
Step :≡ ℕ P(n) → P(n+1)
ind : (t0 : Init) (step : Step) → Π(n:ℕ),P(n) :≡
  0 ↦ t0
  n+1 ↦ step n f(n)

Why

We need to have a type that has one element, to represent True.

Formation

𝟙 : Type

Introduction

x : 𝟙

Elimination

C : Type
elim : (c:C) 𝟙 → C :≡ x ↦ c

ind : (C : 𝟙 → Type) (c : C(x)) → Π(x:𝟙), C(x) :≡ x ↦ c

Why

We need to have a type that has no element, which is used to represent falsity.

Formation

𝟘 : Type

Introduction

Elimination

C : Type
f : 𝟘 → C

C : 𝟘 → Type
f : Π(x:𝟘), C(x)

Why

We need to represents booleans i.e. a type with two elements, true or false.

Formation

Boolean : Type

Introduction

0 : Boolean
1 : Boolean

Elimination

C : Type
elim : (c0:C) (c1:C) → Boolean → C :≡
  0 ↦ c0
  1 ↦ c1

C : Boolean → Type
ind : (c0:C(0)) (c1:C(1)) → Π(x:Boolean), C(x) :≡
  0 ↦ c0
  1 ↦ c1

Why

We need to represents symbols i.e. unique instances (they are only equal to themselves an nothing else).

Formation

Symbol : Type

Introduction

Symbol#mk : String → Symbol
:name :≡ Symbol#mk("name")

Elimination

Behaves like a FinSet where elements are all the symbols that have been introduced so far.

Why

Why do we need to introduce this new type?

Formation

What is the name of that type?

Introduction

How to build instances of that type?

Elimination

How to use instances of that type?

Why

The identity type internalizes the notion of equality (or identification) within the type theory. Given two terms a and b of the same type A, the identity type a = b is the type of evidences that a and b are equal.

Formation

A : Type
a, b : A
IdA(a, b) : U
a = b :≡ IdA(a, b)

Introduction

refl : Π(a:A), a = a

Elimination

C : A → U
f : ∏(x,y:A)∏(p:x=y),C(x) → C(y)
f(x,x,refl(x)) :≡ id(C(x))

C : ∏(x,y:A),x=y → U
c : ∏(x:A),C(x,x,refl(x))
f : ∏(x,y:A), ∏(p:x=y), C(x,y,p)
f(x,x,refl(x)) :≡ c(x)

Why

Lists of things are a common data structures, we need a way to represent them.

Formation

X : Type
List(X) : Type

Introduction

[] : List(X)
cons : X List(X) → List(X)

Elimination

C : Type
elim : (c0 : C) (g : X → C → C) → List(X) → C :≡
  f [] :≡ c0
  f cons(x lst) :≡ g x f(lst)

C : List(X) → Type
c0 : C([])
g : Π(x:X)Π(lst:List(X)), C(lst) → C(cons(x lst))
f : Π(lst:List(X)), C(lst) :≡
  [] ↦ c0
  cons x lst ↦ g x lst f(lst)

Standard map function.

map : List(A) (A → B) → List(B) :≡
  as b ↦
    match as
      [] ↦ []
      cons(a as) ↦ cons(b(a) map(as b))

Why

Computers manipulates bits, let's represent them.

Formation

Bit : Type

Introduction

0 : Bit
1 : Bit

Elimination

C : Type
c0, c1 : C
f : Bit → C :≡
  0 ↦ c0
  1 ↦ c1

C : Bit → Type
c0 : C(0)
c1 : C(1)
f : Π(x:Bit), C(x) :≡
  0 ↦ c0
  1 ↦ c1

Why

Computers manipulate data which are just lists of bits.

Formation

Data :≡ List(Bit)

Why

Programmning languages have a tendency to represent undefined object, which is to say to there is something but we have no idea what that is beyond that point.

Formation

Undefined : Type

Introduction

undefined : Undefined

Elimination

Why

How to represent the absence of a value? By using the unique instance of the Nothing type, isomorphic to 𝟙.

Formation

Nothing : Type

Introduction

nothing : Nothing

Elimination

Why

Assume that a computers tries to map some data received from the network to some type using a given program. Assume an injective mapping, then the algorithm might fail. So, given a piece of data, the algorithm is expected to either provide an instance of some type or nothing. Let's represent that.

Formation

X : Type
Maybe(X) :≡ Nothing + X

Construction

none :≡ left(nothing)
just(x) :≡ right(x)

Why

Finite lists of things that have a known length are common in programming languages, let's defined them.

Formation

X : Type
n : ℕ
Vector(X n) : Type

Introduction

nil : Vector(X zero)
cons(x lst) : X Vector(X n) → Vector(X n+1)

Elimination

🞎

index(lst n) represents the nth element of lst if any, else undefined.

index : List(X 0) Nat → X | Undefined
index([] n) :≡ undefined

index : List(X 1) Nat → X | Undefined
index([x] 0) :≡ undefined
index([x] 1) :≡ x
Given k > 1, then index([x] k) :≡ undefined.

Given index : List(X n) Nat → X | Undefined, lst+x : List(X n+1), and k : Nat, then:

if k < n+1, then index(lst k) :≡ index(lst k)
if k = n+1, then index(lst n+1) :≡ x
if k > n+1, then index(lst k) :≡ undefined

String :≡ List(Nat)

X : Type
Just(X) :≡ 🞎

StrictPartialOrder(X) :≡ 🞎

X : Type
= : X X → Boolean
= is an equality
Set(X =) :≡
  list : List(X)
  e(i) ∈ list, e(j) ∈ list, i ≠ j, e(i) ≠ e(j)

Predicate :≡ X → Boolean