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](https://www.paultaylor.eu/domains/recdic.pdf), 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](https://www.math.ias.edu/Voevodsky/files/files-annotated/Dropbox/Submitted%20papers/Csystem_fromauniverse/Csystem_fromauniverse_new.pdf)). 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: [![extending a context][1]][1] 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.) [1]: https://i.sstatic.net/XSTkzm.png