Categorical semantics of universe levels in dependent type theory

Question

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)?

Answer 1

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.

Modulo coherence issues, a locally cartesian-closed category is a display map category, and so dependent type theories with dependent sums, dependent products, extensional identity types and universes are modelled by locally cartesian-closed categories with universes. (Mike Shulman points this out in the comments, but it's surprisingly difficult to find a definition of universe in this setting, so I thought it would be helpful to spell out.)