Type Theory

x :≡ y means that whenever you read x, you may replace x by y.

Motivation

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)

Motivation

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)

Motivation

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)

Motivation

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

Motivation

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)

Motivation

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)

Motivation

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

Motivation

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)

Motivation

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

Motivation

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?

Motivation

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)

Motivation

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)

Motivation

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

Motivation

Computers manipulate data which are just lists of bits.

Formation

Data :≡ List(Bit)

Motivation

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

Motivation

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) :≡ Undefined + X

Motivation

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)