Model Category

A model category is a way of Interpreting the syntactic expression in the type theory using a category.

Contextual Category

Idea

Syntactic categories of a type theory are a category where the objects are contexts and the morphisms give substitutions.
We need the initial such category to make it grounded.
It needs:

• cosed under small limits and colimits for $\Pi$ and $\Sigma$ types resp.
• Weak equivalences - identity types
• Kan Fibrations - dependent types and subst
• Cofibrations - gives context extensions and gluing.

Definition

Objects: $\mathcal{C}$ - contexts
Morphisms:
Length function $\ell :\mathcal{C}\to \mathbb{N}$
A single empty context $1$, terminal object.
${\mathrm{Ob}}_n$ = set of contexts of length $n$.

Link to original