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 identity-on-objects and 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 dsplayed category $D$ over a category $C$ consists of
such that
…
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$.
As mentioned above, there is a construction $\int$ turning a normal lax functor $F:C \to Prof$ into a functor $\pi_F : \int F \to C$. 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 $dP : C \to Prof$ associated to a functor $P:E \to C$ is obtained by ‘taking fibers’. On objects, it maps $x:C$ to the category $P^{-1}x$ of objects and maps of $E$ mapping to $x$ and its identity arrow, respectively. On morphisms, it maps an arrow $f:x \to y$ to the profunctor $P^{-1}y^{op} \times P^{-1}x \to Set$ mapping a choice of objects $y'$ and $x'$ ‘lifting’ $y$ and $x$ respectively to the set of maps $f^\sharp : x'\to y'$ that project down to $f$, i.e.~the ‘fiber over $f$’ of the arrow part of $P$ (which is defined given two objects).
The category $\int F$ is built as follows:
objects are pairs $(x:C, x' : Fx)$
a morphism $(x,x') \to (y,y')$ is given by a pair of morphisms $(f,f^\sharp)$ where $f:x \to y$ is an arrow in $C$ and $f^\sharp \in Ff(y',x')$
identities are given by picking $1_x : x \to x$ and $1_x^\sharp = 1_x' \in F(1_x)(x',x') = \mathrm{Hom}_{Fx}(x',x')$
composition is defined componentwise: given $(f,f^\sharp) : (x,x') \to (y,y')$ and $(g,g^\sharp):(y,y') \to (z,z')$, the composite is the pair $(gf, \ell_{f,g}(y', f^\sharp, g^\sharp))$, where $(y', f^\sharp, g^\sharp)$ is the equivalence class of the coend defining the composition $Fg \circ Ff$ (see profunctor) and $\ell_{f,g}$ is the laxator of $F$.
Finally, the functor $\pi_F$ simply discards the second component on objects and morphisms.
One can readily observe how this construction reduces to the usual Grothendieck construction when $F$ factors through $Cat$.
The above construction is functorial and turns ‘morphisms of normal lax functors into $Prof$’ into morphisms in $Cat/C$. To describe this, is useful to notice the category of normal lax functors into Prof is given by $Dbl_{normal,lax}^{vertical}(hC, Cat)$, where $hC$ is the casting of $C$, a category, as a double category whose vertical and 2-cells are all trivial.
This category has as objects normal lax double functors $C \to Cat$, where $Cat$ 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 $\phi : F \Rightarrow G$. Its components are given by functors (i.e. vertical cells in $Cat$) $\phi_x : Fx \to Gx$, indexed by objects $x:C$, and squares
indexed by morphisms $f:x\to y$ in $C$. These have, moreover, to satisfy various ‘natural’ conditions of compatibility with horizontal composition of squares in $Cat$ and so on.
The equivalence $\int$ converts this data back to a commutative triangle
The crucial thing to notice here is that, fundamentally, such a functor over $C$ is defined ‘fiberwise’, in the sense that, choosen an object $x:C$, $\int \phi$ has to restrict to a functor $\int\phi_x : \pi_F^{-1}x \to \pi_G^{-1}x$. But these categories are, by definition, $Fx$ and $Gx$, so that $\int \phi_x$ can be naturally defined to be $\phi_x$ itself.
Now what’s left to define is the action of $\int \phi$ on those arrows that cross fibers (in a sense, all the arrows except those that map to identities in $C$ – or, put differently again, the above discussion pinned down the object part of $\int \phi$).
Thus let $(f,f^\sharp):(x,x') \to (y,y')$ be a morphism in $\int F$. We know how to map $(x,x')$ and $(y,y')$ using $\phi_x$ and $\phi_y$ respectively, so that $\int \phi(f,f^\sharp)$ has to be an arrow $(x,\phi_x(x')) \to (y,\phi_y(y'))$. The exact arrow is picked by the last piece of data from the vertical transformation $\phi$, the ‘strength’ $\mathrm{st}^{\phi}$. In fact this is a natural transformation whose components are $\mathrm{st}^{\phi}_{x',y'} : Ff(x',y') \to Gf(\phi_x(x'),\phi_y(y'))$, which is exactly the data needed to define the arrow part of $\int \phi$.
Functoriality of $\int \phi$ is a direct consequence of the properties required to $\phi$, which are spelled out at vertical natural transformation.
The correspondence between categories over $C$ and normal lax functors $C\to Prof$ was observed by Bénabou already in 1972:
A more detailed account of Benaobou’s work on this topic can be found at:
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 October 27, 2022 at 07:38:57. See the history of this page for a list of all contributions to it.