Category of Contexts (Semantics)

Carmell’s contextual categories. Interpretation of the syntactic expressions in type theory. Let $\mathbf{T}$ be a type theory with standard rules. The category of contexts $\mathcal{C}(\mathbf{T})$ is defined as follows:

• Objects are finite contexts $\left[x_0:A_0,...\right]$.
• Maps are context morphisms or substitutions.
• Equality of contexts and morphisms are up to definitional equality and renaming.

Contextual categories from universes

A universe in a context category $\mathcal{E}$ consists of:

• an object $U$
• a morphism $\pi :\tilde{U}\to U$
• for every $A:\Gamma \to U$ a choice of pullback square:

This allows us to construct contexts within a universe. Write $(\Gamma ;A,B)$ for $((\Gamma ;A);B)$.

*What is $\tilde{U}$?

References

riehl-hott-semantics (definition 2.1.1)