A displayed category over a category $C$ is the “classifying map” of a category over $C$. That is, it is equivalent to the data of a category $D$ and a functor $F:D\to C$, but organized differently as a “functor” associating to each object or morphism of $C$ the fiber over it. The operation (which is an equivalence) taking a displayed category to the corresponding functor $F:D\to C$ is a generalization of the Grothendieck construction.
Displayed categories are particularly useful in type theory (especially internal categories in homotopy type theory) and to preserve the principle of equivalence, since they allow a more “category-theoretic” formulation of various notions (such as Grothendieck fibrations and strict creation of limits) that, if stated in terms of a functor $F:D\to C$, would involve equality of objects.
A displayed category over a category $C$ is a lax functor from $C$, regarded as a bicategory with only identity 2-cells, to the bicategory Span.
Better, it is a lax double functor from $C$, regarded as a double category “horizontally” with only identity vertical arrows and 2-cells, to the (pseudo) double category $Span$ with sets as objects, functions as vertical arrows, and spans as horizontal arrows. Although this produces an equivalent notion, it is better because a displayed functor is then a vertical transformation between such lax double functors.
A displayed category may equivalently be described as a normal lax functor from $C$ to Prof (either the bicategory or the double category, as appropriate), meaning one that strictly preserves identities. Formally, this is because $Prof = Mod(Span)$, where $Mod(-)$ denotes the double category of horizontal monads and modules, and $Mod$ is a right adjoint to the inclusion of virtual double categories and normal (lax) functors into all (lax) functors; see (CS, Prop. 5.14).
Equivalently, it is a double profunctor between $C$ and the terminal double category $1$, i.e., a double presheaf on $C$.
The category over $C$ corresponding to a displayed category $D:C\to Span$ is the pullback
Where $Span_*=Span(Set_*)$ is the bicategory (or double category) of pointed sets and pointed spans. This is a strict pullback, which exists in the 2-category of bicategories (or double categories) and lax functors because the projection $Span_* \to Span$ is not just lax but strong. Equivalently, it is the pullback
where $Prof_*$ consists of pointed categories and pointed profunctors, a pointed profunctor $H:(A,a_0)⇸(B,b_0)$ being equipped with an element of $H(a_0,b_0)$.
This construction induces an equivalence of categories $Disp(C) \to Cat/C$, which restricts to the following equivalences:
A displayed category factors through the inclusion $Set \hookrightarrow Span$ (or equivalently $Set \hookrightarrow Prof$) if and only if $F:D\to C$ is a discrete opfibration. Similarly, it factors through $Set^{op}$ if and only if $F$ is a discrete fibration.
A factorization of a displayed category $C\to Prof$ through the inclusion $Cat^{op} \hookrightarrow Prof$ (as corepresentable profunctors) is equivalent to giving $F:D\to C$ the structure of a cloven prefibred category, i.e. equipped with a choice of weakly cartesian liftings. The factorization is a pseudofunctor precisely when $F:D\to C$ is a Grothendieck fibration; in this case we see the usual Grothendieck construction of a pseudofunctor.
Similarly, factorizations through $Cat\hookrightarrow Prof$ corresponds to cloven Grothendieck (pre)opfibrations.
An arbitrary displayed category $C\to Prof$ is a pseudofunctor if and only if $F:D\to C$ is a Conduché functor, i.e. an exponentiable morphism in $Cat$.
The correspondence between categories over $C$ and normal lax functors $C\to Prof$ was observed by
The term “displayed category”, and the applications to type theory, are due to:
An unpacking of the definition as lax functors into Span is in 2.2 of
Also cited above:
Last revised on September 8, 2019 at 07:25:44. See the history of this page for a list of all contributions to it.