A displayed category over a base category $\mathrm{𝒞︀}$ packages the data of a category that “lies over” $\mathrm{𝒞︀}$: each object and each morphism of $\mathrm{𝒞︀}$ is equipped with a fiber of objects and morphisms displayed atop it. It consists of

1. For each object $𝑥:{\mathrm{𝒞︀}}_0$, a type of displayed objects lying over $𝑥$. We write for a displayed object over $𝑥$.
2. For each morphism $𝑓:\mathrm{𝒞︀}(𝑥,𝑦)$ and displayed objects and , a set of displayed morphisms lying over $𝑓$. We write such a displayed morphism as or , subscripting the arrow with the base morphism $𝑓$ it lies over.
3. A displayed composition operation. For $𝑓:𝑥\to 𝑦$ and $𝑔:𝑦\to 𝑧$ with displayed morphisms and , there is a displayed morphism lying over the composite $𝑓\star 𝑔$.
4. For each , a displayed identity lying over ${\text{𝗂𝖽}}_{𝑥}$.

5. Left-unitality, displayed: for all , a heterogeneous equality

6. Right-unitality, displayed: for all , a heterogeneous equality

7. Associativity, displayed: for all , , over $𝑓:𝑥\to 𝑦$, $𝑔:𝑦\to 𝑧$, $ℎ:𝑧\to 𝑤$, a heterogeneous equality

Because the type of displayed morphisms depends on the base morphism $𝑓$, the two sides of each displayed law inhabit different displayed hom-sets — those indexed by the two sides of the corresponding base-category equation. Each displayed law is therefore a heterogeneous equality $𝑎{=}_{𝑝}𝑏$: a path from $𝑎$ to $𝑏$ lying over the base path $𝑝$, rather than an equation within a single fixed set.

Concretely, this definition models the one used in the Cubical standard library [1].

A displayed category is to a category as a dependent type is to a context. In this way, displayed categories are effectively dependent categories, as we present the structure of as a category parametrized by the structure of $\mathrm{𝒞︀}$.

Displayed categories were introduced by Ahrens and Lumsdaine [2]. The point is that a displayed category over $\mathrm{𝒞︀}$ is equivalent to the data of a category $\mathrm{𝒟︀}$ together with a functor $𝐹:\mathrm{𝒟︀}\to \mathrm{𝒞︀}$, but presented as families indexed by the objects and morphisms of $\mathrm{𝒞︀}$ — so that constructions like Grothendieck fibrations can be defined without ever invoking equality of objects.