A displayed category over a category is the “classifying map” of a category over . That is, it is equivalent to the data of a category and a functor , but organized differently as a “functor” associating to each object or morphism of the fiber over it. The operation (which is an equivalence) taking a displayed category to the corresponding functor 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 , would involve equality of objects.
A displayed category over a category is a lax functor from , regarded as a bicategory with only identity 2-cells, to the bicategory Span.
Better, it is a lax double functor from , regarded as a double category “horizontally” with only identity vertical arrows and 2-cells, to the (pseudo) double category 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 to Prof (either the bicategory or the double category, as appropriate), meaning one that strictly preserves identities. Formally, this is because , where denotes the double category of horizontal monads and modules, and 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 and the terminal double category , i.e., a double presheaf on .
The category over corresponding to a displayed category is the pullback
Where 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 is not just lax but strong. Equivalently, it is the pullback
where consists of pointed categories and pointed profunctors, a pointed profunctor being equipped with an element of .
This construction induces an equivalence of categories , which restricts to the following equivalences:
A displayed category factors through the inclusion (or equivalently ) if and only if is a discrete opfibration. Similarly, it factors through if and only if is a discrete fibration.
A factorization of a displayed category through the inclusion (as corepresentable profunctors) is equivalent to giving the structure of a cloven prefibred category, i.e. equipped with a choice of weakly cartesian liftings. The factorization is a pseudofunctor precisely when is a Grothendieck fibration; in this case we see the usual Grothendieck construction of a pseudofunctor.
Similarly, factorizations through corresponds to cloven Grothendieck (pre)opfibrations.
An arbitrary displayed category is a pseudofunctor if and only if is a Conduché functor, i.e. an exponentiable morphism in .
The correspondence between categories over and normal lax functors 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 May 8, 2020 at 16:05:26. See the history of this page for a list of all contributions to it.