The Comprehension Construction

In 2017 Emily Riehl and I posted a paper [1] on the arXiv entitled “The comprehension construction.” and we blogged about it on the n-Category Café. That post explains the use of the term comprehension in the title of that paper.

I have reproduced it here to show off some Haskell hacking I’ve been indulging in to support the typesetting of category theoretic diagrams in blog posts. To do this I’ve used LaTeX to generate SVG images, from diagrams specified using packages such as PGF/TikZ, which are then inlined directly into HTML pages.

What is the comprehension construction?

The comprehension construction is somehow analogous to both the straightening and the unstraightening constructions introduced by Lurie in his development of the theory of quasi-categories. Most people use the term ∞-categories as a rough synonym for quasi-categories, but we reserve this term for something more general: the objects in any ∞-cosmos. There is an ∞-cosmos whose objects are quasi-categories and another whose objects are complete Segal spaces. But there are also more exotic ∞-cosmoi whose objects model (∞,n)-categories or fibered (∞,1)-categories, and our comprehension construction applies to any of these contexts.

The input to the comprehension construction is any cocartesian fibration between ∞-categories together with a third ∞-category . The output is then a particular homotopy coherent diagram that we refer to as the comprehension functor. In the case , the comprehension functor defines a “straightening” of the cocartesian fibration. In the case where the cocartesian fibration is the universal one over the quasi-category of small ∞-categories, the comprehension functor converts a homotopy coherent diagram of shape into its “unstraightening,” a cocartesian fibration over .

The fact that the comprehension construction can be applied in any ∞-cosmos has an immediate benefit. The codomain projection functor associated to an ∞-category defines a cocartesian fibration in the slice ∞-cosmos over , in which case the comprehension functor specializes to define the Yoneda embedding.

Classical comprehension

The comprehension scheme in ZF set theory asserts that for any proposition involving a variable whose values range over some set there exists a subset comprised of those elements for which the formula is satisfied. If the proposition is represented by its characteristic function , then this subset is defined by the following pullback of the canonical monomorphism . For that reason, is often called the subobject classifier of the category and the morphism is regarded as being its generic subobject. On abstracting this point of view, we obtain the theory of elementary toposes.

The Grothendieck construction as comprehension

What happens to the comprehension scheme when we pass from the 1-categorical context just discussed to the world of 2-categories?

A key early observation in this regard, due to Ross Street I believe, is that we might usefully regard the Grothendieck construction as an instance of a generalised form of comprehension for the category of categories. This analogy becomes clear when we observe that the category of elements of a functor may be formed by taking the pullback: Here the projection functor on the right, from the slice of the category of sets under the one point set, is a discrete cocartesian fibration. It follows, therefore, that this pullback is also a 2-pullback and that its left-hand vertical is a discrete cocartesian fibration.

Street’s point of view is (roughly) that in a 2-category it is the (suitably defined) discrete cocartesian fibrations that play the role that the sub-objects inhabit in topos theory. Then the generic sub-object becomes a discrete cocartesian fibration in with the property that pullback of along 1-cells provides us with equivalences between each hom-category and the category of discrete cocartesian fibrations over in .

This account, however, glosses over one important point; thus far we have only specified that each comparison functor should act by pulling back along each 1-cell . We have said nothing about how, or weather, this action might extend in any reasonable way to 2-cells in !

The key observation in that regard is that for any fixed “representably defined” cocartesian fibration in a (finitely complete) 2-category , we may extend pullback to define a pseudo-functor . This carries each 1-cell to the pullback of along and its action on a 2-cell is constructed in the manner depicted in the following diagram: Here we make use of the fact that is a cocartesian fibration in order to lift the whiskered 2-cell to a cocartesian 2-cell . Its codomain 1-cell may then be factored through , using the pullback property of the front square, to give a 1-cell over as required. Standard (essential) uniqueness properties of cocartesian lifts may now be deployed to provide canonical isomorphisms and and to prove that these satisfy required coherence conditions.

It is this 2-categorical comprehension construction that motivates the key construction of our paper.

Comprehension and 2-fibrations

In passing, we might quickly observe that the 2-categorical comprehension construction may be regarded as being but one aspect of the theory of 2-fibrations. Specifically the totality of all cocartesian fibrations and cartesian functors between them in is a 2-category whose codomain projection is a cartesian 2-fibration, it is indeed the archetypal such gadget. Under this interpretation, the lifting construction used to define the pseudo-functor is quite simply the typical cartesian 2-cell lifting property characteristic of a 2-fibration.

In an early draft of our paper, our narrative followed just this kind of route. There we showed that the totality of cocartesian fibrations in an ∞-cosmos could be assembled to give the total space of a kind of cartesian fibration of (weak) 2-complicial sets. In the end, however, we abandoned this presentation in favour of one that was more explicitly to the point for current purposes. Watch this space, however, because we are currently preparing a paper on the complicial version of this theory which will return to this point of view. For us this has become a key component of our work on foundations of complicial approach to -category theory.

An ∞-categorical comprehension construction

In an ∞-cosmos , by which we mean a category enriched over quasi-categories that admits a specified class of isofibrations and certain simplicially enriched limits, we may again define to be a cocartesian fibration representably. That is to say, is a cocartesian fibration if it is an isofibration in the specified class and if is a cocartesian fibration of quasi-categories for every ∞-category . Then a direct “homotopy coherent” generalisation of the 2-categorical construction discussed above demonstrates that we define an associated comprehension functor: The image lands in the maximal Kan complex enriched subcategory of the quasi-categorically enriched category of cocartesian fibrations and cartesian functors over , so the comprehension functor transposes to define a map of quasi-categories whose codomain is defined by applying the homotopy coherent nerve.

Straightening as comprehension

The “straightening” of a cocartesian fibration into a homotopy coherent diagram is certainly one of early highlights in Lurie’s account of quasi-category theory. Such functors are intrinsically tricky to construct, since that process embroils us in specifying an infinite hierarchy of homotopy coherent data.

We may deploy the ∞-categorical comprehension to provide a alternative approach to straightening. To that end we work in the ∞-cosmos of quasi-categories and let , then observe that the comprehension functor is itself the straightening of . Indeed, it is possible to use the constructions in our paper to extend this variant of unstraightening to give a functor of quasi-categories: Here is the (large) quasi-category constructed by taking the homotopy coherent nerve of (the maximal Kan complex enriched subcategory of) . So the objects of correspond bijectively to “straight” simplicial functors . We should confess, however, that we do not explicitly pursue the full construction of this straightening functor there.

Unstraightening as comprehension

In the ∞-categorical context, the Grothendieck construction is christened unstraightening by Lurie. It is inverse to the straightening construction discussed above.

We may also realise unstraightening as comprehension. To that end we follow Ross Street’s lead by taking to be a quasi-category of pointed quasi-categories and apply the comprehension construction to the “forget the point” projection . The comprehension functor thus derived defines a quasi-categorical analogue of Lurie’s unstraightening construction. In an upcoming paper we use the quasi-categorical variant of Beck’s monadicity theorem to prove that this functor is an equivalence. We also extend this result to certain other ∞-cosmoi, such as the ∞-cosmos of (co)cartesian fibrations over a fixed quasi-category.

Constructing the Yoneda embedding

Applying the comprehension construction to the cocartesian fibration in the slice ∞-cosmos , we obtain a map that carries an element to the groupoidal cartesian fibration . This provides us with a particularly explicit model of the Yoneda embedding, whose action on hom-spaces is easily computed. In particular, this allows us to easily demonstrate that the Yoneda embedding is fully-faithful and thus that every quasi-category is equivalent to the homotopy coherent nerve of some Kan complex enriched category.

References