The total category of a displayed category over $\mathrm{𝒞︀}$ collects the displayed data into a single category. Its objects are pairs of an object $𝑥$ of $\mathrm{𝒞︀}$ with an object over it, and its morphisms are pairs of a morphism $𝑓:𝑥\to 𝑦$ with a displayed morphism over $𝑓$.

Projecting out the first components is a functor . Constructions presented displayed — algebras, Eilenberg–Moore categories — get their forgetful functor for free as this projection.

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.

Given a displayed category over a category $\mathrm{𝒞︀}$ and another displayed category over , the total category of , we can define , the displayed total category of , as a displayed category over $\mathrm{𝒞︀}$.

Given any displayed monoidal category ${𝑀}^{\text{𝙳}}$ over $\text{𝖥𝗋𝖾𝖾𝖬𝗈𝗇}(𝑋)$ with an interpretation $𝜄:𝑋⇝{𝑀}^{\text{𝙳}}$, we may construct a global section $\text{𝖥𝗋𝖾𝖾𝖬𝗈𝗇}(𝑋)\to {𝑀}^{\text{𝙳}}$. We refer to this as the global elimination principle of $\text{𝖥𝗋𝖾𝖾𝖬𝗈𝗇}(𝑋)$.

Given a displayed category over a category $\mathrm{𝒞︀}$ and a functor $𝐹:\mathrm{𝒟︀}\to \mathrm{𝒞︀}$, the reindexing of along $𝐹$ is a displayed category over $\mathrm{𝒟︀}$. It is simply the portion of over the image of $𝐹$.

For categories $\mathrm{𝒞︀}$ and $\mathrm{𝒟︀}$, we can define the weakening of $\mathrm{𝒟︀}$ over $\mathrm{𝒞︀}$ as a displayed category over $\mathrm{𝒞︀}$ which trivially displays a copy of $\mathrm{𝒟︀}$ over each object of $\mathrm{𝒞︀}$.

Let $𝑃$ be a presheaf on a category $\mathrm{𝒞︀}$. The category of elements of $𝑃$ is the displayed category over $\mathrm{𝒞︀}$ whose displayed objects over $𝑐$ are the elements $𝑝\in 𝑃𝑐$, and whose displayed morphisms over $𝑓:𝑐\to 𝑑$ from $𝑝$ to $𝑞$ are proofs that $(𝑃𝑓)(𝑞)=𝑝$.

Since $𝑃𝑐$ is a set, there is at most one displayed morphism over each $𝑓$ between given elements: a morphism of elements is a morphism of $\mathrm{𝒞︀}$ that happens to carry $𝑞$ back to $𝑝$. Its total category is the classical category of elements $\int 𝑃$, and a universal element of $𝑃$ is exactly a terminal object of $\int 𝑃$.

Given a displayed category over $\mathrm{𝒞︀}$ and an object $𝑐:{\mathrm{𝒞︀}}_0$, the fiber of over $𝑐$ is the category whose objects are the displayed objects , and whose morphisms are the vertical morphisms , those lying over the identity.

Identities are the displayed identities. The displayed composite of two vertical morphisms lies over ${\text{𝗂𝖽}}_{𝑐}\star {\text{𝗂𝖽}}_{𝑐}$ rather than ${\text{𝗂𝖽}}_{𝑐}$, so composition in the fiber transports it along ${\text{𝗂𝖽𝖫}}_{{\text{𝗂𝖽}}_{𝑐}}$.

A section $𝑠$ of a displayed category over $\mathrm{𝒞︀}$ chooses

1. for each object $𝑐:{\mathrm{𝒞︀}}_0$, a displayed object , and
2. for each morphism $𝑓:𝑐\to 𝑑$, a displayed morphism lying over $𝑓$,

such that $𝑠({\text{𝗂𝖽}}_{𝑐})={\text{𝗂𝖽}}_{𝑠(𝑐)}$ and $𝑠(𝑓\star 𝑔)=𝑠(𝑓)\star 𝑠(𝑔)$.

A section is to a displayed category what a dependent function $(𝑎:𝐴)\to 𝐵(𝑎)$ is to a dependent type: it picks a displayed datum over every base datum.

The total bicategory of a displayed bicategory over $\mathrm{𝒦︀}$ packages the base and the displayed data together, one dimension up from the total category of a displayed category.

• Its 0-cells are pairs of a 0-cell of $\mathrm{𝒦︀}$ and a displayed 0-cell over it.
• Its hom-category from to is the total category of the displayed hom-category . So a 1-cell is a pair and a 2-cell is a pair .
• Identities, composition, unitors and associator are pairs of the base structure and the displayed structure over it, and the triangle and pentagon hold because they hold in the base and, over that, in the displayed bicategory.

Projecting to first components is a pseudofunctor whose unit and composition comparisons are identity 2-cells.