Martin-Löf Type Theory

1. Type Theory as a Foundation

Source: this video.
Unlike classical mathematics, which is typically built on top of first-order logic and axiomatic set theory (such as ZFC), Martin-Löf Type Theory is a foundational system that stands entirely on its own.

• Self-Contained: It does not assume or rely on any pre-existing logic, set theory, or category theory. Instead, logic and mathematics are derived directly from the rules of type theory.
• A Theory of Constructions: Rather than focusing on "what is the case" (the domain of traditional logic), type theory defines how mathematical objects are built (constructed) and manipulated (taken apart and reassembled).
• The Geometric Interpretation: We could translate the structural elements of type theory into geometric language:
  • A Type corresponds to a Space.
  • An Element of a type corresponds to a Point in that space.
  • Proofs are treated as constructions (for example, a formal proof of a statement is represented as a tree-like deduction construction).

2. Basic Concepts and Notations

Types and Elements

We write $A\text{ type}$ to declare that $A$ is a type (or a "space"). If $t$ is a construction of type $A$, we write:

This states that $t$ is an element (or a point) of $A$.
Unlike set theory—where an element can exist independently of any set and we later test the proposition $x\in S$—in type theory, an element always belongs to a specific type by definition. All the terms of a type share a pre-defined "structured". The statement $t:A$ is a "judgment", not a proposition.

Contexts and Dependency

MLTT is a dependent type theory, meaning that types and points can depend on other points. We collect our assumptions and free variables in a context (traditionally denoted by the Greek letter $\mathrm{\Gamma }$).
A dependent type is written as:

Examples of Dependency in Standard Mathematics:

1. The space of real vectors ${\mathbb{R}}^n$ depends on a natural number $n$. In type theory, this is expressed under the context of $n$:$$n:\mathbb{N}⊢{\mathbb{R}}^n\text{ type}$$
2. The closed interval $[a,b]$ depends on the real endpoints $a$ and $b$, as well as proof/evidence $p$ that $a\le b$:$$a:\mathbb{R},b:\mathbb{R},p:(a\le b)⊢[a,b]\text{ type}$$

Judgemental Equality ($\equiv$)

We establish when two constructions or types are definitionally identical using judgemental equality:

• $\mathrm{\Gamma }⊢A\equiv B$ (judgementally equal types)
• $\mathrm{\Gamma }⊢s{\equiv }_{A}t$ (judgementally equal points in $A$)

Judgemental equality is checked purely by the computational rules of the system (we will see later).

3. The Geometric Picture: Fibrations and Sections

To visualize dependency, we use the language of fiber bundles (fibrations) [1, 2]:

      Total Space: Σ (x:A). B(x)
       +-----------------------+
       |       / \  <-- Fiber B(x)
       |      |   |            |
       |      |   |            |  
       |       \ /             |
       +--------|-------|-------+
                | Projection
                v
       Base Space A:
       ---------x-------y------->

• The Base Space: The type $A$ sits "downstairs" as the base space.
• The Fiber: For each point $x:A$, there is a space $B(x)$ sitting vertically above it. We call $B(x)$ the fiber over $x$.
• The Total Space: If we collect all the fibers $B(x)$ together over the entire base $A$, we obtain a larger space known as the total space (representing the dependent sum, $\sum (x:A).B(x)$). There is a natural projection map from this total space back down to $A$.
• The Section: A dependent element $x:A⊢t(x):B(x)$ is a rule that assigns to each point $x:A$ a point $t(x)$ in the fiber $B(x)$. Geometrically, this traces out a continuous curve cutting across the fibers, known as a section of the family $B$ over $A$.

4. Core Type Constructions

Every type constructor in MLTT is defined by four sets of rules: formation (how to build the type), introduction (how to build elements of the type), elimination (how to use/destruct elements), and computation/uniqueness (how the introduction and elimination rules interact).

A. The Dependent Sum ($\mathrm{\Sigma }$-Type)

The dependent sum is denoted as:

• Geometric Meaning: The total space of the family $B$ over $A$.
• Elements: Ordered pairs $(s,t)$ where $s:A$ and $t:B(s)$.
• Operations (Eliminators): Projections ${\pi }_1$ and ${\pi }_2$, which split a pair into its constituent parts:$${\pi }_1(u):A\text{and}{\pi }_2(u):B({\pi }_1(u))$$
• Equations:
  • Computation ($\beta$-rules): Extracting components from a constructed pair:$${\pi }_1(s,t){\equiv }_{A}s\text{and}{\pi }_2(s,t){\equiv }_{B(s)}t$$
  • Uniqueness ($\eta$-rule): Assuring every element in the sum is structurally a pair:$$({\pi }_1(u),{\pi }_2(u)){\equiv }_{\sum (x:A).B(x)}u$$

Special Case: Binary Product ($A\times B$)

If the fiber $B$ does not actually vary with $x$ (i.e., $B$ is a constant space independent of $A$), the dependent sum simplifies to the ordinary cartesian product $A\times B$.

• Why "Sum"? If the base space $A$ consists of discrete points $\{a,b,c\}$, the dependent sum is the disjoint union (the sum of the elements) of the fibers: $B(a)\uplus B(b)\uplus B(c)$.

B. The Dependent Product ($\mathrm{\Pi }$-Type)

The dependent product is denoted as:

• Geometric Meaning: The space of all sections of the family $B$ over $A$.
• Elements: Functions. We construct them using "lambda abstraction notation":$$\lambda x:A.e:B(x)$$Where $e:B(x)$ is an expression that may contain the variable $x$.
• Operations (Eliminators): Application. If we have a function $f:\mathrm{\Pi }(x:A).B(x)$ and a point $t:A$, we can apply $f$ to $t$ to obtain a point in the fiber:$$ft:B(t)$$This could be written as$$\frac{\mathrm{\Gamma }⊢f:\mathrm{\Pi }(x:A).B(x)\mathrm{\Gamma }⊢t:A}{\mathrm{\Gamma }⊢ft:B(t)}$$
• Equations:
  • Computation ($\beta$-rule / Substitution): Applying a lambda abstraction substitutes the argument into the expression:$$(\lambda x:A.e)t{\equiv }_{B(t)}e[x:=t]$$
  • Uniqueness ($\eta$-rule): Every element of a $\mathrm{\Pi }$-type behaves as a function:$$\lambda x:A.fx{\equiv }_{\mathrm{\Pi }(x:A).B(x)}f$$
  • Extensionality Rule: Two functions are judgementally equal if they yield equal results for all inputs:$$\frac{\mathrm{\Gamma },x:A⊢u(x){\equiv }_{B(x)}v(x)}{\mathrm{\Gamma }⊢(\lambda x:A.u(x)){\equiv }_{{\mathrm{\Pi }}_{(x:A)}B(x)}(\lambda x:A.v(x))}$$

Special Case: Function Space ($A\to B$)

If $B$ is constant and independent of $A$, the dependent product simplifies to the ordinary function space $A\to B$.

• Why "Product"? For a discrete base $A=\{a,b,c\}$, a section must choose one element from $B(a)$, one from $B(b)$, and one from $B(c)$. The number of possible sections is the product of the sizes of the fibers: $|B(a)|\times |B(b)|\times |B(c)|$. If the fibers are of equal size, this yields exponentiation $|B{|}^{|A|}$.

C. The Natural Numbers ($\mathbb{N}$)

The natural numbers are defined as an inductive type:

• Constructors (Introduction):$$0:\mathbb{N}\text{and}S:\mathbb{N}\to \mathbb{N}(\text{Successor})$$
• The Induction Principle (Eliminator): To use or prove properties over $\mathbb{N}$, we are given an induction term. Given a type family $P$ over $\mathbb{N}$ (i.e., $n:\mathbb{N}⊢P(n)\text{ type}$), the induction operator is a function of the type:$${\text{ind}}_{\mathbb{N}}:P(0)\to ({\mathrm{\Pi }}_{(k:\mathbb{N})}(P(k)\to P(S(k))))\to {\mathrm{\Pi }}_{(n:\mathbb{N})}P(n)$$
• Computation Equations:
  • Base Case: Applying induction to $0$ yields the base step $s:P(0)$:$${\text{ind}}_{\mathbb{N}}st0{\equiv }_{P(0)}s$$
  • Inductive Step: Applying induction to a successor $S(n)$ recursively computes the step:$${\text{ind}}_{\mathbb{N}}st(S(n)){\equiv }_{P(S(n))}tn({\text{ind}}_{\mathbb{N}}stn)$$

Note: I didn't understand this yet.

D. Finite Types

The Empty Type ($\mathbf{0}$)

• Elements: None.
• Eliminator (Ex Falso Quodlibet): If we are given an element of the empty type, we can construct an element of any other type $A$:$$\frac{t:\mathbf{0}}{\text{exfalso}(t):A}$$

The Unit Type ($\mathbf{1}$)

• Elements: A single element, denoted by $\ast$ or $()$:$$():\mathbf{1}$$
• Uniqueness Equation: Any two elements of the unit type are judgementally equal:$$s{\equiv }_{\mathbf{1}}t$$

The Booleans ($\mathbf{2}$)

• Elements: true and false.
• Eliminator: Conditionals (if-then-else) represented by case analysis:$$\text{if }b\text{ then }s\text{ else }t$$

E. Universes ($\mathcal{U}$)

To talk about types as mathematical objects themselves, we introduce a Universe $\mathcal{U}$, which is a "type of types". Its elements are types:

• Avoiding Paradoxes: Having a single universe contain itself ($\mathcal{U}:\mathcal{U}$) leads to Girard's Paradox (the type-theoretic equivalent of Russell’s Paradox). To avoid this, MLTT uses a predicative hierarchy of universes:$${\mathcal{U}}_0:{\mathcal{U}}_1:{\mathcal{U}}_2:\dots$$
• Cumulativity: Universes are cumulative. If a type is small enough to fit in ${\mathcal{U}}_i$, it also belongs to any larger universe:$$\text{If }A:{\mathcal{U}}_i,\text{ then }A:{\mathcal{U}}_{i+1}$$
• Closure: Each universe is closed under all the basic type-forming operations (such as $\mathrm{\Sigma }$-types, $\mathrm{\Pi }$-types, finite types, and natural numbers).
• Representing Type Families: Using universes, we can formally represent a dependent type $B$ over $A$ simply as an ordinary function mapping $A$ to the universe:$$B:A\to \mathcal{U}$$

5. Type Theory as a Formal System

To define MLTT rigorously as a formal system, we specify it using hypothetical judgments (judgments made under a context $\mathrm{\Gamma }$, which acts as a set of available hypotheses) and rules of inference.

1. The Four Judgement Forms

The system is built on exactly four types of judgments:

1. Type Validity:$$\mathrm{\Gamma }⊢A\text{ type}$$Meaning: Under context $\mathrm{\Gamma }$, $A$ is a well-formed type.
2. Term Membership:$$\mathrm{\Gamma }⊢t:A$$Meaning: Under context $\mathrm{\Gamma }$, $t$ is a valid construction (element) of type $A$.
3. Type Equality:$$\mathrm{\Gamma }⊢A\equiv B$$Meaning: Under context $\mathrm{\Gamma }$, types $A$ and $B$ are definitionally (judgementally) equal.
4. Term Equality:$$\mathrm{\Gamma }⊢s{\equiv }_{A}t$$Meaning: Under context $\mathrm{\Gamma }$, $s$ and $t$ are definitionally (judgementally) equal elements of type $A$.

2. Rules of Inference

The transitions between these judgments are defined using formal rules of inference, which are written in a fraction-like notation:

• Premises ($P_1\dots P_n$): The judgments above the line that must already be derived.
• Conclusion ($C$): The new judgment below the line that we are permitted to derive once the premises are established.

Example:
The Dependent Product ($\mathrm{\Pi }$-Type) is "made" of 4 inference rules

1. Formation Rule (The Box Exists)

2. Introduction Rule (What the "Points" Look Like)
   This rule tells you exactly what kind of objects are allowed to live inside this new space. It says: "If you can construct a term $e$ of type $B(x)$ under the assumption that $x:A$, then you can wrap it in a $\lambda$ to make a point in the $\mathrm{\Pi }$-space."

Now we know the points in this space are functions (or paths/sections).

3. Elimination Rule (How to Use the Points)
   This rule tells you how to interact with an object from this space. It says: "If you have a point $f$ in the $\mathrm{\Pi }$-space, and you have a point $t$ in the base space $A$, you are allowed to combine them via application ($ft$) to land in the vertical fiber $B(t)$."

Now we know these functions can be evaluated on inputs.

4. Computation Rule (How the Points Move / Interact)
   This final rule locks in the actual mechanical behavior. It bridges the Introduction rule (how we made the function) and the Elimination rule (how we used it) using Judgemental Equality ($\equiv$). It says: "If you build a function using $\lambda$ and immediately evaluate it using an input $t$, that is definitionally identical to just substituting $t$ into the original expression."

Example: how would this formal system machine begin?