[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).


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
%
$\Hom_{\Ty}$
$\Ty(\underbrace{σ}_{\rlap{∈ \Hom_𝒞(Δ, Γ)}}) : \Ty(Γ) ⟶ \Ty(Δ), \ldots$
type substitutions
$% $
$\bigg\vert\Tm\bigg(\int_𝒞 \Ty^{\,\op} \bigg)\bigg\vert$
$\Tm(Δ, A), \Tm(Γ, B), \ldots$
terms of a given type over a given context
%
$\Hom_{\Tm}$
$\Tm(\underbrace{σ}_{\rlap{∈ \Hom_𝒞(Δ, Γ) \text{ and } \Ty(σ)(B) = A }}) : \Tm(Γ, B) ⟶ \Tm(Δ, A), \ldots$
term substitutions
$% $

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

Tags:

Updated: