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