September | 2025 | Bartosz Milewski's Programming Cafe

Previously: Models of (Dependent) Type Theory.

There is a deep connection between mathematics and programming. Computer programs deal with such mathematical objects as numbers, vectors, monoids, functors, algebras, and many more. We can implement such structures in most programming languages. For instance, here’s the definition of natural numbers in Haskell:

data Nat where
  Z :: Nat           -- zero
  S :: Nat -> Nat    -- successor

There is a problem, though, with encoding the laws that they are supposed to obey. These laws are expressed using equalities. But not all equalities are created equal. Take, for instance, this definition of addition:

plus :: Nat -> Nat -> Nat
plus Z n = n
plus (S n) m = S (plus n m)

The first clause tells us that $0 + n$ is equal to $n$ . This is called definitional equality, since it’s just part of the definition. However, if we reverse the order of the addends and try to prove $n + 0 = n$ , there is no obvious shortcut. We have to prove it the hard way! This second type of equality is called propositional.

In traditional mathematics equality is treated as a relation. Two things are either equal or not. In type theory, on the other hand, equality is a type. It’s a type of proofs of equality. When you postulate that two things are equal, you specify the type of proofs that you are willing to accept.

Equality is a dependent type, because it depends on the values that are being compared. For a pair of values of the type $A$ , the identity (or equality) type is denoted by $\text{Id}_A$ :

$\frac{a, b \colon A}{\text{Id}_A (a, b) \colon \text{Type}}$

(In this notation, assumptions are listed above the horizontal line.)

You’ll also see $\text{Id}_A(a, b)$ written as $a =_A b$ , or even $a = b$ , if the type $A$ is obvious from the context.

When two values are not equal, this type is uninhabited. Otherwise it’s inhabited by proofs, or witnesses, of equality. This is consistent with the propositions as types interpretation of type theory.

For the identity type to be useful, we have to have a way to populate it with values — proofs of equality. We do that by providing an introduction rule:

$\frac{a \colon A}{\text{refl}(a) \colon \text{Id}_A(a, a)}$

The constructor $\text{refl}$ generates a witness to the obvious fact that, for every $a$ , $a = a$ . Here, $\text{refl}$ is the abbreviation of reflexivity.

At first sight it doesn’t seem like we have gained anything by turning equality into a type. Indeed, if $\text{refl}$ were the only inhabitant of $\text{Id}_A$ , we’d just buy ourselves a lot of headaches for nothing. The trouble is that, if there is a type $\text{Id}_A(a, b)$ , then there’s also a type $\text{Id}_{\text{Id}_A(a,b)}$ (type of equality of proofs of equality), and so on, ad infinitum. This used to be a bane of Martin Löf type theory, but it became a bounty for Homotopy Type Theory. So let’s imagine that the identity type may have non-trivial inhabitants. We’ll call these inhabitants paths. The trivial paths generated by $\text{refl}$ are degenerate do-nothing loops.

But first, let’s consider the identity elimination rule: the mapping out of the identity type. What data do we need to provide in order to define a function from a path $p \colon \text{Id}_A(x, y)$ to some type $D$ ? In full generality, $D$ should be a dependent type family parameterized by the path $p$ as well as its endpoints $x$ and $y$ :

$x, y \colon A, \; p \colon \text{Id}_A (x, y) \vdash D(x, y, p) \colon \text{Type}$

Our goal is to define a $D$ -valued mapping $J$ that works for any path in $A$ :

$x, y \colon A, \; p \colon \text{Id}_A(x, y) \vdash J(x, y, p) \colon D(x, y, p)$

The trick is to realize that there is only one family of constructors of the identity type, $\text{refl}(a)$ , so it’s enough to specify how $J$ is supposed to act on it. We do this by providing a dependent function $d$ (a dependent function is a function whose return type depends on the value of its argument):

$a \colon A \vdash d(a) \colon D(a, a, \text{refl}(a))$

This is very similar to constructing a mapping out of a Boolean by specifying its action on the two constructors, $\text{True}$ and $\text{False}$ . Except that here we have a whole family of constructors $\text{refl}(a)$ parameterized by $a$ .

This is enough information to uniquely determine the action of $J$ on any path, provided it agrees with $d$ along $\text{refl}$ :

$J(a, a, \text{refl}(a)) = d(a)$

This procedure for defining mappings out of identity types is called path induction.

Categorical Model

We’ll build a categorical interpretation of identity types making as few assumptions as possible. We’ll model $\text{Id}_A$ as a fibration:

$\text{Id}_A \xrightarrow{\pi} A \times A$

The introduction rule asserts the existence of the arrow:

$A \xrightarrow{\text{refl}} \text{Id}_A$

For any given $a \colon A$ , this arrow selects a diagonal element of the identity type, $\text{Id}_A(a, a)$ . When projected down to $A \times A$ using $\pi$ , it lands on the diagonal of $A \times A$ . In a cartesian category, the diagonal is defined by the arrow $\Delta \colon A \to A \times A$ , so we have:

$\Delta = \pi \circ \text{refl}$

In other words, there is a factorization of the diagonal arrow.

The elimination rule starts with defining a dependent type $D$ , which can be modeled as a fibration $\rho$ :

$D \xrightarrow{\rho} \text{Id} \xrightarrow{\pi} A \times A$

We provide a dependent function $d$ , which is interpreted as an arrow $d : A \to D$ that maps $a$ to an element $d(a)$ of $D(a, a, \text{refl}(a))$ . So, when projected back to $\text{Id}_A$ using $\rho$ , it produces the same element as $\text{refl}(a)$

$\rho \circ d = \text{refl}$

Given these assumptions, there exists a mapping:

$x, y \colon A, p \colon \text{Id}_A(x, y) \vdash J(x, y, p) \colon D(x, y, p)$

which is interpreted as a section $\text{Id}_A \to D$ . The section condition is:

$\rho \circ J = id_{\text{Id}_A}$

This mapping is unique if we assume that it agrees with $d$ when restricted to $\text{refl}$ :

$J \circ \text{refl} = d$

Consequently, we can illustrate the path induction rule using a single commuting diagram:

If the outer square commutes then there is a unique diagonal arrow that makes the two triangles commute. The similarity to the lifting property of homotopy theory is not accidental, as we’ll see next.

Next: Modeling Identity Types.

Previously: (Weak) Factorization Systems.

It’s been known since Lambek that typed lambda calculus can be modeled in a cartesian closed category, CCC. Cartesian means that you can form products, and closed means that you can form function types. Loosely speaking, types are modeled as objects and functions as arrows.

More precisely, objects correspond to contexts— which are cartesian products of types, with the terminal object representing the empty context. Arrows correspond to terms in those contexts.

Mathematicians and computer scientist use special syntax to formalize type theory that is used in lambda calculus. For instance a typing judgment:

$\vdash A \colon \text{Type}$

states that $A$ is a type. The turnstile symbol is used to separate contexts from judgments. Here, the context is empty (nothing on the left of the turnstile). Categorically, this means that $A$ is an object.

A more general context $\Gamma$ is a product of objects $A_1 \times A_2 \times ...$ . The judgment:

$\Gamma \vdash A \colon \text{Type}$

tells us that the type $A$ may depend on other types $A_1 \times A_2 \times ...$ , in which case $A$ is a type constructor. The canonical example of a type constructor is a list.

A term $t$ of type $A$ in some context $\Gamma$ is written as:

$\Gamma \vdash t \colon A$

We interpret it as an arrow from the cartesian product of types that form $\Gamma$ to the object $A$ :

$\Gamma \xrightarrow{t} A$

Things get more interesting when we allow types to not only depend on other types, but also on values. This is the real power of dependent types à la Martin-Löf.

For instance, the judgment:

$a \colon A \vdash B(a) \colon \text{Type}$

defines a single-argument type family. For every argument $a$ of type $A$ it produces a new type $B(a)$ . The canonical example of a dependent type is a counted vector, which encodes length (a value of type $\mathbb N$ ) in its type.

Categorically, we model a type family as a fibration given by an arrow $\pi \colon B \to A$ . The type $B(a)$ is a fiber $\pi^{-1} a$ .

In the case of counted vectors, the projection gives the length of the vector.

In general, a type family may depend on multiple arguments, as in:

$a_1 \colon A_1, a_2 \colon A_2, ... , a_n \colon A_n \vdash B(a_1, a_2, ..., a_n) \colon \text{Type}$

Here, each type in the context may depend on the values defined by its predecessor. For instance, $A_2$ may depend on $a_1$ , $A_3$ may depend on $a_1$ and $a_2$ , and so on.

Categorically, we model such a judgment as a tower of fibrations:

$B \xrightarrow{\pi_n} A_n ... \xrightarrow{\pi_2} A_2 \xrightarrow{\pi_1} A_1$

Notice that the context is no longer a cartesian product of types but rather an ordered series of fibrations.

A term in a dependently typed system has to satisfy an additional condition: it has to map into the correct fiber. For instance, in the judgment:

$a \colon A \vdash t(a) \colon B(a)$

not only $t$ depends on $a$ , but so does the type $B(a)$ . If we model $t$ as an arrow $A \to B$ , we have to make sure that $t(a)$ is projected back to $a$ . Categorically, we call such maps sections:

$\pi \circ t = id_A$

In other words, a section is an arrow that is a right inverse of a projection, .

Thus a well-formed vector-valued term produces, for every $n \colon \mathbb N$ , a vector of lenght $n$ .

In general, a term:

$a_1 \colon A_1, a_2 \colon A_2, ... , a_n \colon A_n \vdash t \colon B$

is interpreted as a section $A_n \xrightarrow{t} B$ of the projection $\pi_n$ .

At this point one usually introduces the definitions of dependent sums and products, which requires the modeling category to be locally cartesian closed. We’ll instead concentrate on the identity types, which are closely related to homotopy theory.

Next: Identity Types.

Bartosz Milewski's Programming Cafe

September 2025

Identity Types

Categorical Model

Models of (Dependent) Type Theory

Top Posts

License

Blogroll

Follow Me

Archives