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.