Curry–Howard Isomorphism

As AI becomes stronger and stronger in coding and math, I feel that type theory will become vastly more popular. Code and math generated by AI need things like formal verification to check that it is hallucination free. I've been reading a bit of Egbert Rijke's introduction to homotopy type theory ⟦cite:Rij25⟧ . I find the part about Curry–Howard isomorphism/correspondence particularly interesting. Indeed, one can think of a mathematical proof as some kind of program. For this post, I will write a short exposition of these ideas.

Dependent Type Theory

Dependent type theory is a system of inference rules.

$$ \frac{\mathcal{H}_1 \quad \mathcal{H}_2 \quad \cdots \quad \mathcal{H}_n}{\mathcal C}. $$

Here each letter is a judgement.

A judgement in Martin-Löf's dependent type theory is one of the following:

$A$ is a (well-formed) type in context $\Gamma$, written $\Gamma \vdash A\ \mathrm{type}$.
$A$ and $B$ are judgmentally equal types in context $\Gamma$, written $\Gamma \vdash A \equiv B\ \mathrm{type}$.
$a$ is an element of type $A$ in context $\Gamma$, written $\Gamma \vdash a : A$.
$a$ and $b$ are judgmentally equal elements of type $A$ in context $\Gamma$, written $\Gamma \vdash a \equiv b : A$.

A context is a finite list of variable declarations

$$ x_1 : A_1,\ x_2 : A_2(x_1),\ \ldots,\ x_n : A_n(x_1, \ldots, x_{n-1}) $$

such that, for every $1 \leq i \leq n$, the type $A_i(x_1, \ldots, x_{i-1})$ is well-formed in the context of the preceding declarations:

$$ x_1 : A_1,\ \ldots,\ x_{i-1} : A_{i-1}(x_1, \ldots, x_{i-2}) \vdash A_i(x_1, \ldots, x_{i-1})\ \mathrm{type}. $$

Let $A$ be a type in context $\Gamma$. A family of types $B$ over $A$ in context $\Gamma$ is a type $B(x)$ in context $\Gamma, x : A$; that is,

$$ \Gamma, x : A \vdash B(x)\ \mathrm{type}. $$

Equivalently, $B(x)$ is a type indexed by $x : A$ in context $\Gamma$. Let $B$ be a family of types over $A$ in context $\Gamma$. A section of $B$ over $A$ in context $\Gamma$ is an element $b(x)$ of type $B(x)$ in context $\Gamma, x : A$; that is,

$$ \Gamma, x : A \vdash b(x) : B(x). $$

Equivalently, $b(x)$ is an element of type $B(x)$ indexed by $x : A$ in context $\Gamma$.

The specific inferences can be found in Rijke. Specifically there are dependent rules such as:

The dependent product introduction rule:
$$ \frac{\Gamma, x : A \vdash b(x) : B(x)}{\Gamma \vdash \lambda x.\, b(x) : \prod_{(x : A)} B(x)}\;\lambda. $$
The dependent sum introduction rule:
$$ \frac{\Gamma \vdash a : A \quad \Gamma \vdash b : B(a)}{\Gamma \vdash (a,b) : \sum_{(x : A)} B(x)}. $$

Identity Types

For $a,b:A$, we want $a=b$ to be a type and its elements thought of as identifications of them, defined via inductive types.

Let $A$ be a type and let $a : A$. The identity type of $a$ is the inductive family of types $a =_A x$, indexed by $x : A$, generated by the constructor

$$ \operatorname{refl}_a : a =_A a. $$

Thus, for $a,b : A$, the type $a =_A b$ (also written $\operatorname{Id}_A(a,b)$) is the type of identifications of $a$ with $b$.

The identity type is specified by the following rules:

The formation rule:
$$ \frac{\Gamma \vdash a : A}{\Gamma, x : A \vdash a =_A x\ \mathrm{type}}. $$
Once $a$ is an element of $A$, we may form, for every $x : A$, the type of identifications from $a$ to $x$.
The introduction rule:
$$ \frac{\Gamma \vdash a : A}{\Gamma \vdash \operatorname{refl}_a : a =_A a}. $$
Every element is identified with itself, by its reflexivity identification $\operatorname{refl}_a$.
The elimination rule, also called identity elimination or path induction: if $C(x,p)$ is a type in context $\Gamma, x : A, p : a =_A x$, then
$$ \frac{\Gamma \vdash a : A \quad \Gamma, x : A, p : a =_A x \vdash C(x,p)\ \mathrm{type}}{\Gamma \vdash \operatorname{ind\text{-}eq}_a : C(a,\operatorname{refl}_a) \to \prod_{(x : A)} \prod_{(p : a =_A x)} C(x,p)}. $$
To define something for every identification $p : a =_A x$, it is enough to define it for the reflexivity identification $\operatorname{refl}_a$.
The computation rule:
$$ \frac{\Gamma \vdash a : A \quad \Gamma, x : A, p : a =_A x \vdash C(x,p)\ \mathrm{type}}{\Gamma, c : C(a,\operatorname{refl}_a) \vdash \operatorname{ind\text{-}eq}_a(c,a,\operatorname{refl}_a) \equiv c : C(a,\operatorname{refl}_a)}. $$
When path induction is applied to reflexivity, it computes to the value $c$ with which the construction began.

Curry–Howard Isomorphism

The Curry–Howard correspondence reads propositions as types and proofs as elements of those types. Thus, to prove a proposition $P$ is to construct a term $p : P$; a proof can be viewed as a program, and its proposition as the program's specification.

$$ \begin{array}{c c} \text{Logic} & \text{Type theory} \\ \hline \text{propositions} & \text{types} \\ \text{proofs} & \text{elements} \\ \text{predicates} & \text{type families} \\ \top & 1 \\ \bot & \varnothing \\ P \lor Q & P + Q \\ P \land Q & P \times Q \\ P \Rightarrow Q & P \to Q \\ \neg P & P \to \varnothing \\ \exists x : A.\, P(x) & \sum_{(x : A)} P(x) \\ \forall x : A.\, P(x) & \prod_{(x : A)} P(x) \\ a = b & a =_A b \end{array} $$

Contractible Types

A type $A$ is contractible if it has a point $a : A$ together with an identification from $a$ to every element of $A$:

$$ \operatorname{is\text{-}contr}(A) := \sum_{(a : A)} \prod_{(x : A)} a =_A x. $$

For $(a,H) : \operatorname{is\text{-}contr}(A)$, the point $a$ is the center of contraction, and $H(x) : a =_A x$ is its contraction at $x$. Thus, a contractible type is a singleton up to identification.

For a map $f : A \to B$ and an element $b : B$, the fibre of $f$ over $b$ is the type

$$ \operatorname{fib}_f(b) := \sum_{(x : A)} f(x) =_B b. $$

An element of $\operatorname{fib}_f(b)$ is a point $x : A$ together with a path witnessing that $f(x)$ is $b$.

A map $f : A \to B$ is contractible if every fibre of $f$ is contractible. The type expressing this property is

$$ \operatorname{is\text{-}contr}(f) := \prod_{(b : B)} \operatorname{is\text{-}contr}(\operatorname{fib}_f(b)). $$

Thus, over each $b : B$, there is a chosen point of $A$ mapping to $b$, and every other point mapping to $b$ is identified with it.

(10.1.4)

For every $a : A$, the type

$$ \sum_{(x : A)} a =_A x $$

is contractible.

Take $(a,\operatorname{refl}_a)$ as the center of contraction. The contraction is the dependent function

$$ H : \prod_{(x : A)} \prod_{(p : a =_A x)} (a,\operatorname{refl}_a) = (x,p). $$

Define $H$ by path induction on $p$. It suffices to give its value at $x \equiv a$ and $p \equiv \operatorname{refl}_a$, where we set $H(a,\operatorname{refl}_a) := \operatorname{refl}_{(a,\operatorname{refl}_a)}.$

Fundamental Theorem of Identity Types

Let $B$ be a family of types over $A$. For $p : a =_A x$, transport along $p$ is the map

$$ \operatorname{tr}_B(p) : B(a) \to B(x), $$

defined by path induction with $\operatorname{tr}_B(\operatorname{refl}_a)(u) := u$. It carries an element of the fibre over $a$ to the corresponding element of the fibre over $x$.

A map $e : X \to Y$ is an equivalence if the type

$$ \operatorname{is\text{-}equiv}(e) := \prod_{(y : Y)} \operatorname{is\text{-}contr}(\operatorname{fib}_e(y)) $$

is inhabited; that is, every fibre of $e$ is contractible. We write $X \simeq Y$ when there is an equivalence between $X$ and $Y$.

Given families $B$ and $C$ over $A$, a family of maps from $B$ to $C$ is a dependent function

$$ f : \prod_{(x : A)} B(x) \to C(x). $$

It is a family of equivalences if

$$ \prod_{(x : A)} \operatorname{is\text{-}equiv}(f(x)) $$

is inhabited. Thus each individual map $f(x) : B(x) \to C(x)$ is an equivalence.

Let $a : A$, let $B$ be a family of types over $A$, and choose $b : B(a)$. We regard $B(x)$ as a proposed description of the identity type $a =_A x$, with $b$ playing the role of reflexivity at $a$. Path induction gives a canonical family of maps

$$ \operatorname{encode}_{B,b} : \prod_{(x : A)} (a =_A x) \to B(x), \qquad \operatorname{encode}_{B,b}(x,p) := \operatorname{tr}_B(p)(b). $$

For a point $x : A$, the map $\operatorname{encode}_{B,b}(x,-)$ takes an identification $p : a =_A x$ and transports the chosen element $b$ from the fibre $B(a)$ to the fibre $B(x)$. Thus it converts a path from $a$ to $x$ into a proposed representation of that path at $x$. When $x$ is $a$ and $p$ is reflexivity, no transport occurs, so $\operatorname{encode}_{B,b}(a,\operatorname{refl}_a) \equiv b$.

(11.2.2)

The family $\operatorname{encode}_{B,b}$ is a family of equivalences if and only if the total space

$$ \sum_{(x : A)} B(x) $$

is contractible.

In other words, to show that a proposed family $B(x)$ correctly describes the identifications $a =_A x$, it suffices to choose a reflexivity-like element $b : B(a)$ and prove that all pairs $(x,y)$ with $y : B(x)$ form one point up to identification. The theorem then guarantees that transporting $b$ along paths gives every element of $B(x)$, uniquely up to identification. It turns the problem of characterizing identity types into the often simpler problem of proving a total space contractible.

Propositions

A type $P$ is a proposition if any two of its elements are identified. The type expressing this property is

$$ \operatorname{is\text{-}prop}(P) := \prod_{(p,q : P)} p =_P q. $$

Thus, a proposition may have no proof, but if it has proofs, they are all equal up to identification. In the Curry--Howard interpretation, this means that only the truth of $P$ matters, not the choice of proof.

A type $A$ is a set if every identity type of $A$ is a proposition. Equivalently,

$$ \operatorname{is\text{-}set}(A) := \prod_{(x,y : A)} \operatorname{is\text{-}prop}(x =_A y). $$

In expanded form, this says that for $x,y : A$ and $p,q : x =_A y$, there is an identification $p =_{(x =_A y)} q$. Hence a set may have many elements, but there is at most one way, up to identification, for two fixed elements to be equal.

The Univalence Axiom

A universe $\mathcal U$ is a type whose elements are themselves types. For $A,B : \mathcal U$, an identification $p : A =_{\mathcal U} B$ determines an equivalence

$$ \operatorname{idtoequiv}_{A,B}(p) : A \simeq B, $$

defined by identity elimination with $\operatorname{idtoequiv}_{A,A}(\operatorname{refl}_A) := \operatorname{id}_A$.

The univalence axiom asserts that the canonical map

$$ \operatorname{idtoequiv}_{A,B} : (A =_{\mathcal U} B) \to (A \simeq B) $$

is an equivalence for every $A,B : \mathcal U$.

Thus, in a univalent universe, types are identified exactly when they are equivalent. Equality of types contains no more and no less information than an equivalence between them.

References

[Rij25] Egbert Rijke. Introduction to Homotopy Type Theory. Cambridge Studies in Advanced Mathematics. Vol. 219. Cambridge University Press. 2025.