nLab
displayed category

Displayed categories

Displayed categories

Idea

A displayed category over a category CC is the “classifying map” of a category over CC. That is, it is equivalent to the data of a category DD and a functor F:DCF:D\to C, but organized differently as a “functor” associating to each object or morphism of CC the fiber over it. The operation (which is an equivalence) taking a displayed category to the corresponding functor F:DCF: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:DCF:D\to C, would involve equality of objects.

Definition

A displayed category over a category CC is a lax functor from CC, regarded as a bicategory with only identity 2-cells, to the bicategory Span.

Better, it is a lax double functor from CC, regarded as a double category “horizontally” with only identity vertical arrows and 2-cells, to the (pseudo) double category SpanSpan 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 CC to Prof (either the bicategory or the double category, as appropriate), meaning one that strictly preserves identities. Formally, this is because Prof=Mod(Span)Prof = Mod(Span), where Mod()Mod(-) denotes the double category of horizontal monads and modules, and ModMod 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 CC and the terminal double category 11, i.e., a double presheaf on CC.

Correspondence to slices

The category over CC corresponding to a displayed category D:CSpanD:C\to Span is the pullback

D Span * C Span \array{ D & \to & Span_* \\ \downarrow & & \downarrow \\ C & \to & Span }

Where Span *=Span(Set *)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 *SpanSpan_* \to Span is not just lax but strong. Equivalently, it is the pullback

D Prof * C Prof \array{ D & \to & Prof_* \\ \downarrow & & \downarrow \\ C & \to & Prof }

where Prof *Prof_* consists of pointed categories and pointed profunctors, a pointed profunctor H:(A,a 0)(B,b 0)H:(A,a_0)⇸(B,b_0) being equipped with an element of H(a 0,b 0)H(a_0,b_0).

This construction induces an equivalence of categories Disp(C)Cat/CDisp(C) \to Cat/C, which restricts to the following equivalences:

  • A displayed category factors through the inclusion SetSpanSet \hookrightarrow Span (or equivalently SetProfSet \hookrightarrow Prof) if and only if F:DCF:D\to C is a discrete opfibration. Similarly, it factors through Set opSet^{op} if and only if FF is a discrete fibration.

  • A factorization of a displayed category CProfC\to Prof through the inclusion Cat opProfCat^{op} \hookrightarrow Prof (as corepresentable profunctors) is equivalent to giving F:DCF: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:DCF:D\to C is a Grothendieck fibration; in this case we see the usual Grothendieck construction of a pseudofunctor.

  • Similarly, factorizations through CatProfCat\hookrightarrow Prof corresponds to cloven Grothendieck (pre)opfibrations.

  • An arbitrary displayed category CProfC\to Prof is a pseudofunctor if and only if F:DCF:D\to C is a Conduché functor, i.e. an exponentiable morphism in CatCat.

References

The correspondence between categories over CC and normal lax functors CProfC\to Prof was observed by

  • Jean Bénabou, Distributors at work, Notes by Thomas Streicher from lectures given at TU Darmstadt, 2000, pdf

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 9, 2020 at 05:42:14. See the history of this page for a list of all contributions to it.