Type Theory

→

Function type.

Formation Rule

\frac{A : 𝒰 B : 𝒰}{A \to B : 𝒰} .

Introduction Rule

λ-abstraction.

\frac{a : A b : B}{λ (a) . b : A \to B} .

Computation Rule

β-conversion or β-reduction.

\frac{a : A b : B}{(λ (a) . b) (a) \equiv b : B} .

Uniqueness Principle

η-conversion or η-expansion.

\frac{a : A b : B}{b \equiv λ (a) . b (a) : A \to B} .

α-conversion

\frac{λ (x) . f (x)}{λ (y) . f (y)} .

Currying

\frac{}{c (a, b) \equiv c (a) (b)} .

Right Associativity

\frac{}{A \to B \to C \equiv A \to (B \to C)} .

Constant Function

\frac{b : B a : A}{λ (a) . b : A \to B} .

Universe

Introduction Rule

\frac{}{𝒰_{i} : 𝒰_{i + 1}} .

Cumulativity

\frac{A : 𝒰_{i}}{A : 𝒰_{i + 1}} .

Dependent Type (type family)

Finite Set

Fin : ℕ \to 𝒰 .

Constant Dependent Type

B : 𝒰 ⊢ λ (a) . B : A \to 𝒰 .

Dependent →

Dependent function type, Π-type.

Formation Rule

\frac{A : 𝒰 a : A ⊢ B : 𝒰}{(a : A) \to B : 𝒰} .

Introduction Rule

\frac{a : A ⊢ b : B}{λ (a : A) . b : (a : A) \to B} .

Elimination Rule

\frac{b : (a : A) \to B a : A}{b (a) : B [a/x]} .

Computation Rule

Uniqueness Principle

\frac{b : (a : A) \to B}{b \equiv λ (a) . b : (a : A) \to B} .

(a : A) \to B \equiv A \to B (x, y : A) \to B (x, y) \equiv (x : A) \to (y : A) \to B (x, y) .

Example

fmax \equiv n \mapsto n_{n + 1} : (n : ℕ) \to Fin (n + 1) .

Polymorphic Function

\frac{A : 𝒰, x : A}{{id}_{A} \equiv x} .

A, B, C : 𝒰, c : C | swap \equiv b \to a \to c .

×

Product type, cartesian product.

Formation Rule

\frac{a : A b : B}{A \times B : 𝒰} .

Introduction Rule

\frac{a : A b : B}{(a, b) : A \times B} .

Recursion Principle

\begin{array}{l} {rec}_{A \times B} (C, c, (a, b)) \equiv c (a) (b), \\ {rec}_{A \times B} : (C : 𝒰) \to (A \to B \to C) \to (A \times B) \to C . \end{array}

Projection

\begin{array}{l} {pr}_{1} \equiv {rec}_{A \times B} (A, λ (a) . λ (b) . a), \\ {pr}_{1} : A \times B \to A . \\ {pr}_{2} \equiv {rec}_{A \times B} (B, λ (a) . λ (b) . b), \\ {pr}_{2} : A \times B \to B . \end{array}

Induction Principle

\begin{array}{l} {ind}_{A \times B} (C, c, (a, b)) \equiv c (a) (b), \\ {ind}_{A \times B} : (C : (A \times B) \to 𝒰) \to ((a : A) \to (b : B) \to C ((a, b))) \to (x : A \times B) \to C (x) . \end{array}

Uniqueness Principle

Propositional uniqueness principle.

\begin{array}{l} {uniq}_{A \times B} ((a, b)) \equiv {refl}_{(a, b)}, \\ {uniq}_{A \times B} : (x : A \times B) \to (({pr}_{1} (x), {pr}_{2} (x)) = x) . \end{array}

From category-theoretic perspective, we define product A × B to be left adjoint to the 'exponential' B → C.

𝟏

Unit type.

Formation Rule

\frac{}{𝟏 : 𝒰} .

Introduction Rule

\frac{}{* : 𝟏} .

Recursion Principle

\begin{array}{l} {rec}_{𝟏} (C, c, *) \equiv c, \\ {rec}_{𝟏} : (C : 𝒰) \to C \to 𝟏 \to C . \end{array}

Induction Principle

\begin{array}{l} {ind}_{𝟏} (C, c, *) \equiv c, \\ {ind}_{𝟏} : (C : 𝟏 \to 𝒰) \to C (*) \to (x : 𝟏) \to C (x) . \end{array}

Uniqueness Principle

Propositional uniqueness principle.

\begin{array}{l} {uniq}_{𝟏} \equiv {refl}_{*}, \\ or {uniq}_{𝟏} \equiv {ind}_{𝟏} (λ (x) . x = *, {refl}_{*}), \\ {uniq}_{𝟏} : (x : 𝟏) \to (x = *) . \end{array}

Dependent ×

Dependent pair type, Σ-type.

Formation Rule

\frac{A : 𝒰 a : A ⊢ B : 𝒰}{(a : A) \times B (a) : 𝒰} .

Introduction Rule

\frac{a : A ⊢ B (a) : 𝒰 a : A b : B [a/x]}{(a, b) : (x : A) \times B (x)} .

((a : A) \times B) \equiv (A \times B) .

\begin{array}{l} {pr}_{1} ((a, b)) \equiv a, \\ {pr}_{1} : ((a : A) \times B (a)) \to A . \\ {pr}_{2} : (p : (a : A) \times B (a)) \to B ({pr}_{1} (p)) . \end{array}

Recursion Principle

\begin{array}{l} {rec}_{(a : A) \times B (a)} (C, c, (a, b)) \equiv c (a) (b), \\ {rec}_{(a : A) \times B (a)} : (C : 𝒰) \to ((a : A) \to B (a) \to C) \to ((a : A) \times B (a)) \to C . \end{array}

Induction Principle

Dependent eliminator.

\begin{array}{l} C (p) \equiv B ({pr}_{1} (p)), \\ {pr}_{2} ((a, b)) \equiv b . \end{array}

\begin{array}{l} {ind}_{(a : A) \times B (a)} (C, c, (a, b)) \equiv c (a) (b), \\ \begin{array}{l} {ind}_{(a : A) \times B (a)} : (C : ((a : A) \times B (a)) \to 𝒰) \\ \to ((a : A) \to (b : B (a)) \to C ((a, b))) \\ \to (p : (a : A) \times B (a)) \to C (p) . \end{array} \end{array}

Uniqueness Principle

Propositional uniqueness principle.

See this.

Axiom of choice

\begin{array}{l} ac (g) \equiv (x \mapsto {pr}_{1} (g (x)), x \mapsto {pr}_{2} (g (x))), \\ ac : ((x : A) \to (y : B) \times R (x, y)) \to ((f : A \to B) \times (x : A) \to R (x, f (x))) . \end{array}

+

Sum type, coproduct type.

Formation Rule

\frac{A : 𝒰 B : 𝒰}{A + B : 𝒰} .

Introduction rules

\frac{A : 𝒰 B : 𝒰 a : A}{inl (a) : A + B}, \frac{A : 𝒰 B : 𝒰 b : B}{inr (b) : A + B} .

Recursion Principle

Case analysis'

\begin{array}{l} {rec}_{A + B} (C, c_{0}, c_{1}, inl (a)) \equiv c_{0} (a), \\ {rec}_{A + B} (C, c_{0}, c_{1}, inr (b)) \equiv c_{1} (b), \\ {rec}_{A + B} : (C : 𝒰) \to (A \to C) \to (B \to C) \to (A + B) \to C . \end{array}

Induction Principle

\begin{array}{l} {ind}_{A + B} (C, c_{0}, c_{1}, inl (a)) \equiv c_{0} (a), \\ {ind}_{A + B} (C, c_{0}, c_{1}, inr (b)) \equiv c_{1} (b), \\ {ind}_{A + B} : (C : (A + B) \to 𝒰) \to ((a : A) \to C (inl (a))) \to ((b : B) \to C (inr (b))) \to (x : A + B) \to C (x) . \end{array}

𝟎

Empty type.

Formation Rule

\frac{}{𝟎 : 𝒰} .

Introduction Rule

-.

Recursion Principle

Principle of explosion. Canonical function.

\begin{array}{l} {rec}_{𝟎} : (C : 𝒰) \to 𝟎 \to C . \end{array}

Induction Principle

\begin{array}{l} {ind}_{𝟎} : (C : 𝟎 \to 𝒰) \to (x : 𝟎) \to C (x) . \end{array}

𝟐

Boolean type.

Formation Rule

\frac{}{𝟐 : 𝒰} .

Introduction rules

\frac{}{0_{𝟐} : 𝟐}, \frac{}{1_{𝟐} : 𝟐} .

Recursion Principle

\begin{array}{l} {rec}_{𝟐} (C, c_{0}, c_{1}, 0_{𝟐}) \equiv c_{0}, \\ {rec}_{𝟐} (C, c_{0}, c_{1}, 1_{𝟐}) \equiv c_{1}, \\ {rec}_{𝟐} : (C : 𝒰) \to C \to C \to 𝟐 \to C . \end{array}

Induction Principle

\begin{array}{l} {ind}_{𝟐} (C, c_{0}, c_{1}, 0_{𝟐}) \equiv c_{0}, \\ {ind}_{𝟐} (C, c_{0}, c_{1}, 1_{𝟐}) \equiv c_{1}, \\ {ind}_{𝟐} : (C : 𝟐 \to 𝒰) \to C (0_{𝟐}) \to C (1_{𝟐}) \to (x : 𝟐) \to C (x) . \end{array}

ℕ

Natural numbers.

Formation Rule

\frac{}{ℕ : 𝒰} .

Introduction Rules

\frac{}{0 : ℕ}, \frac{n : ℕ}{succ (n) : ℕ} .

Recursion Principle

Primitive recursion.

\begin{array}{l} {rec}_{ℕ} (C, c_{0}, c_{s}, 0) \equiv c_{0}, \\ {rec}_{ℕ} (C, c_{0}, c_{s}, succ (n)) \equiv c_{s} (n, {rec}_{ℕ} (C, c_{0}, c_{s}, n)), \\ {rec}_{ℕ} : (C : 𝒰) \to C \to (ℕ \to C \to C) \to ℕ \to C . \end{array}

Induction Principle

\begin{array}{l} {ind}_{ℕ} (C, c_{0}, c_{s}, 0) \equiv c_{0}, \\ {ind}_{ℕ} (C, c_{0}, c_{s}, succ (n)) \equiv c_{s} (n, {ind}_{ℕ} (C, c_{0}, c_{s}, n)), \\ {ind}_{ℕ} : (C : ℕ \to 𝒰) \to C (0) \to ((n : ℕ) \to C (n) \to C (succ (n))) \to (n : ℕ) \to C (n) . \end{array}

Uniqueness Principle

Pattern Matching and Recursion

Propositions As Types

English	Type Theory
True	$𝟏$
False	$𝟎$
A and B	$A \times B$
A or B	$A + B$
If A then B	$A \to B$
A if and only if B	$(A \to B) \times (B \to A)$
Not A	$A \to 𝟎$
For all a : A, P(a) holds	$(a : A) \to P (a)$
There exists a : A such that P(a)	$(a : A) \times P (a)$

a : A, P, Q \to a : A \to P, a : A \to Q .

=

Identity type.

Formation Rule

\frac{A : 𝒰 a : A b : A}{a =_{A} b : 𝒰} .

Introduction Rule

Reflexivity.

\frac{A : 𝒰 a : A}{{refl}_{a} : a =_{A} a} .

Recursion Principle

Indiscernibility of identicals.

\begin{array}{l} {rec}_{=_{A}} (C, a, a, {refl}_{a}) \equiv =_{C (a)}, \\ {rec}_{=_{A}} : (C : A \to 𝒰) \to (a, b : A) \to (p : a =_{A} b) \to C (a) \to C (b) . \end{array}

Induction Principle

Path induction.

\begin{array}{l} {ind}_{=_{A}} (C, c, a, a, {refl}_{a}) \equiv c (a), \\ {ind}_{=_{A}} : (C : (a, b : A) \to (a =_{A} b) \to 𝒰) \to ((a : A) \to C (a, a, {refl}_{a})) \to (a, b : A) \to (p : a =_{A} b) \to C (a, b, p) . \end{array}

Uniqueness Principle

Inductive Types

\begin{matrix} nil : {Vec}_{0} (A), \\ cons : (n : ℕ) \to A \to \end{matrix}

{Vec}_{n} (A) \to {Vec}_{succ (n)} (A) .

\begin{matrix} C : (n : ℕ) \to {Vec}_{n} (A) \to 𝒰, \\ c_{nil} : C (0, nil), \\ c_{cons} : (n : N) \to (a : A) \to (l : {Vec}_{n} (A)) \to C (n, l) \to C (succ (n), cons (a, l)) . \end{matrix}

\begin{matrix} f : (n : N) \to (l : {Vec}_{n} (A)) \to C (n, l), \\ f (0, nil) \equiv c_{nil}, \\ f (succ (n), cons (a, l)) \equiv c_{cons} (n, a, l, f (l)) . \end{matrix}

Theorem

f, g : (n : ℕ) \to E (n), e_{z} : E (0), e_{s} : (n : ℕ) \to E (n) \to E (succ (n)), f (0) = e_{z}, g (0) = e_{z}, (n : ℕ) \to f (succ (n)) = e_{s} (n, f (n)), (n : ℕ) \to g (succ (n)) = e_{s} (n, g (n)), \to f = g .

nil : List (1), cons : 1 \times List (1) \to List (1) .

\begin{matrix} E : List (1) \to 𝒰, \\ e_{nil} : E (nil), \\ e_{cons} : (u : 1) \to (l : List (1)) \to E (l) \to E (cons (u, l)), \\ f : (l : List (1)), \\ f (nil) \equiv e_{nil}, \\ f (cons (u, l)) \equiv e_{cons} (u, l, f (l)) . \end{matrix}

0'' \equiv nil, succ'' (l) \equiv cons (*, l), succ'' : List (1) \to List (1), E : List (1) \to 𝒰, e_{0} : E (0''), e_{s} : (l : List (1)) \to E (l) \to E (succ'' (l)), e_{nil} \equiv e_{0}, e_{cons} (*, l, x) \equiv e_{s} (l, x) . f (0'') \equiv f (nil) \equiv e_{nil} \equiv e_{0}, f (succ'' (l)) \equiv f (cons (*, l)) \equiv e_{cons} (*, l, f (l)) \equiv e_{s} (l, f (l)), f : (l : List (1)) \to E (l), ∴ List (1) = ℕ .

W-Types

W_{a : A} B (a) .

ℕ^{w} \equiv W_{b : 𝟐} {rec}_{𝟐} (𝒰, 0, 1, b) .

list (A) \equiv W_{x : 𝟏 + A} {rec}_{𝟏 + A} (𝒰, 0, a \mapsto 1, x) .

\sup : (a : A) \to (B (a) \to W_{x : A} B (x)) \to W_{x : A} B (x) .

0^{w} \equiv \sup (0_{𝟐}, x \mapsto {rec}_{𝟎} (ℕ^{w}, x)) .

1_{w} \equiv \sup (1_{𝟐}, x \mapsto 𝟎^{w}), {succ}^{w} \equiv n \mapsto \sup (1_{𝟐}, x \mapsto n) .

e : (a : A) \to (f : B (a) \to W_{x : A} B (x)) \to (g : (b : B (a)) \to E (f (b))) \to E (\sup (a, f)) .

e : (a : 𝟐) \to (f : B (a) \to ℕ^{w}) \to (g : B (a) \to ℕ^{w}) \to ℕ^{w} .

ℕ-Algebra

Inductive types are homotopy-initial algebras

Definition

ℕAlg \equiv (C : 𝒰) \times C \times (C \to C) .

ℕ-homomorphism

Definition

h : C \to D, h (c_{0}) = d_{0}, h (c_{s} (c)) = d_{s} (h (c)) for c : C .

NHom ((C, c_{0}, c_{s}), (D, d_{0}, d_{s})) \equiv (h : C \to D) \times (h (c_{0}) = d_{0}) \times (c : C) \to (h (c_{s} (c)) = d_{s} (h (c))) .

A natural numbers object in an (∞, 1)-category of N-algebra.

Homotopy-Initial

{is-homotopy-initial}_{ℕ} (I) \equiv (c : NAlg) \to {is-truncated}_{−2} (NHom (I, C)) .

Theorem

{is-homotopy-initial}_{ℕ} ((ℕ, 0, succ)) .

N-algebras are the algebras for the endofunctor F(X)≡X + 1 of the category of types.

Polynomial Functor

P (X) = (a : A) \times (B (a) \to X) .

W-Algebra

Also called P-algebra.

WAlg (A, B) \equiv (C : 𝒰) \times (a : A) \to (B (a) \to C) \to C .

W-Homomorphism

Also Called P-homomorphism.

f (s_{C} (a, h)) = s_{D} (a, f h) .

{WHom}_{A, B} ((C, s_{C}), (D, s_{D})) \equiv (f : C \to D) \times (a : A) \to (h : B (a) \to C) \to f (s_{C} (a, h)) = s_{D} (a, f h) .

Homotopy-Inductive Type

The General Syntax of Inductive Definitions

Strict Positivity

Generalisations of Inductive Types

Identity Type and Identity System

Pointed Predicate

(A, a_{0}), R : A \to 𝒰, r_{0} : R (a_{0}) .

Pointed

(R, r_{0}), (S, s_{0}), g : (b : A) \to R (b) \to S (b), g (a_{0}, r_{0}) = s_{0} .

ppmap (R, S) \equiv (g : (b : A) \to R (b) \to S (b)) \times (g (a_{0}, r_{0}) = s_{0}) .

Identity System

\begin{matrix} (R, r_{0}) D : (b : A) \to R (b) \to 𝒰, d : D (a_{0}, r_{0}), \\ f : (b : A) \to (r : R (b)) \to D (a_{0}, r_{0}), \\ f (a_{0}, r_{0}) = d . \end{matrix}

Rational Numbers

ℚ \equiv (ℤ \times ℕ) / \approx .

Real Numbers

ℝ

Intensional Type Theory

References

Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. 2013.