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). 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

The term “displayed category”, and the applications to type theory, are due to:

Also cited above:

Last revised on May 29, 2018 at 14:14:21. See the history of this page for a list of all contributions to it.