The rules should be rules of immediate inference; we cannot further analyse them, but only explain them. However, in the end, no explanation can substitute each individual’s understanding.
—Per Martin-Löf

About Type Theory—A Quickstart

Type Theory deals with types and terms with equalities, in the plainest—syntactic—sense of the word, between such types and terms. We refer to equality in this sense (which is not much) as definitional equality.

Judgements

Formally, statements we make about types and terms are called judgements and there are four of them:

  1. \(Γ ⊢ A : \mathbb{U}\)

    This says that A is a type. I am writing 𝕌 instead of \(\mathbf{Type}\). By this, we mean to suggest there is an appropriate universe of types, but more about this later.

  2. \(Γ ⊢ x : A\)

    This says that x is a term of type A.

  3. \(Γ ⊢ A = B : \mathbb{U}\)

    This says that A is equal to B. Duh!

  4. \(Γ ⊢ x = y : A\)

    This says that x and y are equal terms of type A, again definitionally.

So, in the theory, these judgements are derived from axioms (previous judgements) using inference rules.

These derivations, which are essentially finite trees labeled by judgements and inference rules, are the main object of study, and typically derive new judgements from old ones.

The axioms typically include judgements stating the existence of certain basic types and terms.

Observations:

  1. Note that in ordinary Set Theory things like \(a ∈ A\) or \(a = b\) are propositions, while they are judgements here.

  2. In order to say that \(A = B : \mathbb{U}\) of course we have to know that \(A : \mathbb{U}\) and \(B : \mathbb{U}\), etc.

Context

The Γ above is a context. This is the essential feature of Dependent Type Theory: we allow types and terms to depend on (free) variables that may refer to other types and terms.

For example:

\[x : A ⊢ B (x) : \mathbb{U}\]

states that \(B(x)\) is a type that depends on a term \(x\) of type \(A\), a judgement that has previously been derived.

This is of crucial importance: \(B\) is a dependent type.

In general, this can be upgraded to many variables, so that a context can be something like

\[Γ = x_1 : A_1, x_2 : A_2, \dots, x_n : A_n\]

where for each \(m ≤ n\) each type \(A_m\) can only depend on the variables that were declared previously, that is, \(x_1, … , x_{m-1}\).

An observation…

One more example of dependency: let’s say we have the above judgement \(x : A ⊢ B (x) : \mathbb{U}\). So we know that \(B\) is a dependent type. Now, suppose that we can state:

\[x : A ⊢ f (x) : B (x)\]

This means we hold true that \(f(x)\) is term of type \(B(x)\), depending on the variable \(x\), which is a term of type \(A\). So \(f\) is a term of a dependent type \(B\).

But now, suppose that \(B (x)\) does not depend on \(x\), in fact. This is (the analog of) a function from \(A\) to \(B\), which we write

\[x : A ⊢ f (x) : B\]

So, what is a type?

According to Martin-Löf, for each of the four judgements, we must answer one of the following equivalent questions:

  1. What is it? (Ontological—Ancient Greeks)
  2. What do we have to know about it? (Epistemological—Descartes, Kant, …)
  3. What does it <judgement here> mean? (Semantical)

The way Martin-Löf asnwers the question is to call canonical the terms that we can directly “see” that they are the resul of one of the rules, to be distinguished from all the other possible terms, to be deemed noncanonical. Thus, the answer is articulated as follows.

  1. A type \(A\) is defined by prescribing how a canonical term of \(A\) is formed

  2. Two types \(A\) and \(B\) are equal if

    a : A          a : B
-----    &     -----
a : B          a : A

    and

    a = b : A          a = b : B
---------    &     ---------
a = b : B          a = b : A

  3. A term a : A is a method (program) which yields a canonical term of A.

    Example: When we build the naturals we can see that 2 + 2 : ℕ because it computes to suc (2 + 1).

  4. Two arbitrary terms a : A and b : A are equal if, when executed, a and b yield equal canonical elements as a result.

Rules for (definitional) equality

Equality is an equivalence relation, in the sense that it satisfies the three traditional relations, plus it is a congruence with respect to substitution into types and terms:

a = b : A    x : A ⊢ B (x) : 𝕌
-------------------------------
    B (a) = B (b) : 𝕌


a = b : A    x : A ⊢ f (x) : B (x)
----------------------------------
    f (a) = f (b) : B (a)


A = B : 𝕌   a : A
-----------------
     a : B

The rules of the game

In summary, when we try to grasp what a certain type is, that is, when we answer the questions above, we use the following rules:

  1. Formation: this is a judgement that given a certain context we can form the type in question
  2. Introduction: We specify what are the canonical terms and equalities between canonical terms
  3. Elimination: How the newly introduced terms are applied.
  4. Conversion: How the introducton and the elimination rules intereract

An example: Products

  1. Formation:

    x : A ⊢ B (x) : 𝕌
-------------------
Π [x : A] B (x) : 𝕌

  2. Introduction:

    x : A ⊢ f(x) : B (x)
----------------------------
λ x. f (x) : Π [x : A] B (x)

  3. Elimination:

    f : Π [x : A] B (x)    a : A
----------------------------
app(f,a) : B (a)

  4. Conversion:

    λ x. f (x) : Π [x : A] B (x)    a : A
-------------------------------------
app(λ x.f (x), a) = f (a) : B (a)

Interpretations

The HoTT book summarizes the different points of view about type-theoretic operations as follows:

Types Logic Sets Homotopy
A proposition set space
a:A proof element point
B x predicate family of sets fibration
b x : B x conditional proof family of elements section
𝟘, 𝟙 ⊥, ⊤ ∅, {∅} ∅,*
A + B A ∨ B disjoint union coproduct
A x B A ∧ B set of pairs product space
A → B A ⇒ B set of functions function space
Σ [x : A] B x ∃ x:A (B x) disjoint sum total space
Π [x : A] B x ∀ x:A (B x) product space of sections
≡ = \(\{(x,x) | x ∈ A\}\) path space \(A^I\)

Types to build

We will incrementally build a minimal depende type system, including the following types:

  1. The empty type 𝟘

  2. The unit type 𝟙

  3. More general finite types

  4. The natural numbers ℕ

  5. (Dependent) Products—these correspond to Cartesian products

  6. (Dependent) Sums—these generalize disjoint unions

  7. Identity types

    Identity types embody the equality relation not in the shallow definitional sense stated above, but as a proposition. We will see that, far from being a simple equivalence relation, they embody the homotopical and categorical content of HoTT.