[Nottingham Internship] Categories with Families: the true face of Type Theory

I owe special thanks to… guess who? Yes, you’ve figured it out: Paolo Capriotti!

Now it’s time to unleash the power of category theory!

By that, I mean that we’re about to give an algebraic notion of model of type theory via a particular kind of categories: the Categories with Families (which will be abbreviated CwF).

\[\newcommand{\rec}{\mathop{\rm rec}\nolimits} \newcommand{\ind}{\mathop{\rm ind}\nolimits} \newcommand{\inl}{\mathop{\rm inl}\nolimits} \newcommand{\inr}{\mathop{\rm inr}\nolimits} \newcommand{\Hom}{\mathop{\rm Hom}\nolimits} \newcommand{\Ty}{\mathop{\rm Ty}\nolimits} \newcommand{\Tm}{\mathop{\rm Tm}\nolimits} \newcommand{\op}{\mathop{\rm op}\nolimits} \newcommand{\Set}{\mathop{\rm Set}\nolimits} \newcommand{\1}{\mathbf{1}} \newcommand{\b}{\bullet}\]

Categories with Families

a Category with Families (abbreviated CwF):

is given by

• a category $𝒞$, with a terminal object $\b$ (the unit context)

• a presheaf

  \[\Ty : 𝒞^{\,\op} ⟶ \Set\]

• a presheaf from the category of elements of $\Ty$:

  \[\Tm : \bigg(\int_𝒞 \Ty \bigg)^{\,\op} ⟶ \Set\]

• for each $Γ : 𝒞, \; A : \Ty (Γ)$, the following presheaf from the slice category $𝒞/Γ$

  \[\begin{cases} (𝒞/Γ)^{\op} &⟶ \Set \\ (Δ, σ) &⟼ \Tm\big(Δ, \Ty(σ)(A)\big) \end{cases}\]

  is represented by an object $(Γ.A, π_A)$

What does all this mean?

For type theory, the analogy will be the following:

CwF	Type theory
objects \(Γ, Δ, Θ, \ldots\)	contexts \(Δ ≝ (x_1 : A_1, x_2 : A_2(x_1), x_3 : A_3(x_1, x_2), \ldots) \\≝ \b.A_1.A_2(x_1).A_3(x_1, x_2)\ldots \\ Γ ≝ (y_1 : B_1, y_2 : B_2(y_1), y_3 : B_3(y_1, y_2), \ldots)\)
morphisms \(σ : Δ ⟶ Γ, θ : Γ ⟶ Θ, \ldots\)	context morphisms / substitutions \(σ ≝ (t_1 : B_1, t_2 : B_1(t_1), t_3 : B_3(t_1, t_2), \ldots)\)
$\vert\Ty(𝒞)\vert$ \(\Ty(Δ), \Ty(Γ), \ldots\)	types over a given context \(\begin{align*}\lbrace \text{ types over } Δ\rbrace &≝ \lbrace A \mid Δ ⊢ A \rbrace, \\ \lbrace \text{ types over } Γ\rbrace &≝ \lbrace B \mid Γ ⊢ B \rbrace, \ldots \\ \end{align*}\)
$\Hom_{\Ty}$ \(\Ty(\underbrace{σ}_{\rlap{∈ \Hom_𝒞(Δ, Γ)}}) : \Ty(Γ) ⟶ \Ty(Δ), \ldots\)	type substitutions \(\begin{cases} \lbrace B \mid Γ ⊢ B \rbrace &⟶ \lbrace A \mid Δ ⊢ A \rbrace \\ \; B &⟼ B[σ]\end{cases}\)
$\bigg\vert\Tm\bigg(\int_𝒞 \Ty^{\,\op} \bigg)\bigg\vert$ \(\Tm(Δ, A), \Tm(Γ, B), \ldots\)	terms of a given type over a given context \(\begin{align*} \lbrace \text{ terms of type } Δ \text{ over } Δ\rbrace &≝ \lbrace t \mid Δ ⊢ t : A \rbrace, \\ \lbrace \text{ terms of type } Γ \text{ over } Γ\rbrace &≝ \lbrace t \mid Γ ⊢ t : B \rbrace, \ldots \end{align*}\)
$\Hom_{\Tm}$ \(\Tm(\underbrace{σ}_{\rlap{∈ \Hom_𝒞(Δ, Γ) \text{ and } \Ty(σ)(B) = A }}) : \Tm(Γ, B) ⟶ \Tm(Δ, A), \ldots\)	term substitutions \(\begin{cases} \lbrace t \mid Γ ⊢ t : B \rbrace &⟶ \lbrace t \mid Δ ⊢ t : A \rbrace \\ \; t &⟼ t[σ]\end{cases}\)

But first, let’s address why it makes sense to resort to categories (in order to give a model of type theory).