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. This Grothendieck construction is an instance of the T-Grothendieck construction where is the theory of categories.
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 identity-on-objects and 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 consists of
such that
…
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 .
As mentioned above, there is a construction turning a normal lax functor into a functor . Here we spell it out.
But first, let us explictly remark how the opposite construction works. Using notation from Benaboù’s lectures, the normal lax functor associated to a functor is obtained by ‘taking fibers’. On objects, it maps to the category of objects and maps of mapping to and its identity arrow, respectively. On morphisms, it maps an arrow to the profunctor mapping a choice of objects and ‘lifting’ and respectively to the set of maps that project down to , i.e.~the ‘fiber over ’ of the arrow part of (which is defined given two objects).
The category is built as follows:
objects are pairs
a morphism is given by a pair of morphisms where is an arrow in and
identities are given by picking and
composition is defined componentwise: given and , the composite is the pair , where is the equivalence class of the coend defining the composition (see profunctor) and is the laxator of .
Finally, the functor simply discards the second component on objects and morphisms.
One can readily observe how this construction reduces to the usual Grothendieck construction when factors through .
The above construction is functorial and turns ‘morphisms of normal lax functors into ’ into morphisms in . To describe this, is useful to notice the category of normal lax functors into Prof is given by , where is the casting of , a category, as a double category whose vertical and 2-cells are all trivial.
This category has as objects normal lax double functors , where is the proarrow equipment of categories, functors (in the vertical/tight direction), profunctors (in the horizontal/loose direction) and suitable natural transformations as 2-cells. The morphisms are then vertical natural transformations between them.
Let’s spell out the definition of one of these vertical natural transformations . Its components are given by functors (i.e. vertical cells in ) , indexed by objects , and squares
indexed by morphisms in . These have, moreover, to satisfy various ‘natural’ conditions of compatibility with horizontal composition of squares in and so on.
The equivalence converts this data back to a commutative triangle
The crucial thing to notice here is that, fundamentally, such a functor over is defined ‘fiberwise’, in the sense that, choosen an object , has to restrict to a functor . But these categories are, by definition, and , so that can be naturally defined to be itself.
Now what’s left to define is the action of on those arrows that cross fibers (in a sense, all the arrows except those that map to identities in – or, put differently again, the above discussion pinned down the object part of ).
Thus let be a morphism in . We know how to map and using and respectively, so that has to be an arrow . The exact arrow is picked by the last piece of data from the vertical transformation , the ‘strength’ . In fact this is a natural transformation whose components are , which is exactly the data needed to define the arrow part of .
Functoriality of is a direct consequence of the properties required to , which are spelled out at vertical natural transformation.
Let be a functor, call the associated lax normal functor. By requiring a different degree of laxity to or which subcategory of it hits, we can express different properties of :
These and more examples are discussed in Benabou.
The correspondence between categories over and normal lax functors was observed by Bénabou already in 1972:
A more detailed account of Benabou’s work on this topic can be found at:
Jean Bénabou, Distributors at work, Notes by Thomas Streicher from lectures given at TU Darmstadt, 2000, pdf
Graham Manuell?, Monoid extensions and the Grothendieck construction, Semigroup Forum 105 (2022) 488–507 [doi:10.1007/s00233-022-10294-2]
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 February 28, 2024 at 12:57:17. See the history of this page for a list of all contributions to it.