A macrocosm principle for cartesian fibrations
Functors between ∞-categories are given by homotopy coherent diagrams. To avoid having to specify a dizzying array of coherence data, whenever possible practitioners present a homotopy coherent diagram in the form of a *cartesian fibration*, using a lifting property to capture the homotopy coherent functoriality. In this talk, we'll describe a new construction that “straightens” a cartesian fibration into a homotopy coherent diagram that we call its *comprehension functor. *The key component of the construction is expressed by a sort of “macrocosm principle” for cartesian fibrations, summarized by saying that the codomain projection functor from the (∞,2)-category of cartesian fibrations to the (∞,2)-category of ∞-categories is itself a cartesian fibration, in a suitable sense. Time permitting, we explore other applications of the versatile comprehension construction, which specializes both to define an ∞-categorical “unstraightening” functor and to define the Yoneda embedding for any ∞-category.