# Categorical semantics of universe levels in dependent type theory

I know that locally closed cartesian categories provide categorical semantics for type theories with dependent products.

What kind of categories model type theories with infinite universe hierarchies (cumulative or non-cumulative)?

• What are you assuming about the universes? Just closure under $\Pi$? May 1, 2021 at 1:37
• At an elementary level, there isn't going to be an answer to this other than something like "LCCs with universes". More interestingly, there are non-elementary ways to construct universes, e.g. in Grothendieck toposes if there are inaccessible cardinals in the ambient set theory. Is that the sort of thing you're interested in? May 1, 2021 at 2:11

A universe in a category with display maps is a specified display map $$\tilde U \to U$$ (cf. Section 5.5 of Taylor's thesis Recursive Domains, Indexed Category Theory and Polymorphism, or Section 9.6 of Taylor's Practical Foundations of Mathematics; the notation in this answer follows Voevodsky's A C-system defined by a universe in a category). Recall that objects represent contexts, and display maps represent projections from extended contexts, and so this display map can be interpreted as a term $$X : U, x : X \vdash X : U$$. We can extend a context $$\Gamma$$ by a $$U$$-small type $$A$$ (that is, a type in the universe $$U$$) by taking a pullback along the universe:
The morphism $$\Gamma, a : A \to \tilde U$$ is viewed as picking out the type $$A$$ and the term $$a : A$$. Conversely, any display map $$\Gamma, a : A \to \Gamma$$ that fits into a pullback square along the universe may be seen as an extension by a $$U$$-small type in this way.
We can therefore define a hierarchy of (non-cumulative) universes to be a family of display maps $$\{ \tilde U_i \to U_i \}_{i \in \mathbb N}$$ such that each $$U_i$$ is $$U_{i + 1}$$-small. One may additionally want to impose axioms on these universes asserting that they are closed under the type constructors appropriately.