The comprehension construction

TL;DR

This paper introduces the comprehension construction, an analogue of Lurie's unstraightening, which relates functors and cocartesian fibrations in ∞-categories, and demonstrates its applications to Yoneda embeddings and their properties.

Contribution

It constructs the comprehension functor for cocartesian fibrations over ∞-categories and shows its applications to covariant and contravariant Yoneda embeddings.

Findings

The comprehension functor generalizes unstraightening for ∞-categories.

The Yoneda embedding is proven to be fully faithful using the comprehension construction.

Explicit equivalences between ∞-categories and enriched homotopy coherent nerves are established.

Abstract

In this paper we construct an analogue of Lurie's "unstraightening" construction that we refer to as the "comprehension construction". Its input is a cocartesian fibration $p \colon E \to B$ between $\infty$-categories together with a third $\infty$-category $A$. The comprehension construction then defines a map from the quasi-category of functors from $A$ to $B$ to the large quasi-category of cocartesian fibrations over $A$ that acts on $f \colon A \to B$ by forming the pullback of $p$ along $f$. To illustrate the versatility of this construction, we define the covariant and contravariant Yoneda embeddings as special cases of the comprehension functor. We then prove that the hom-wise action of the comprehension functor coincides with an "external action" of the hom-spaces of $B$ on the fibres of $p$ and use this to prove that the Yoneda embedding is fully faithful, providing an explicit equivalence between a quasi-category and the homotopy coherent nerve of a Kan-complex enriched category.