Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$

Theorem 5.6.0.2 (Universality Theorem). Let $\operatorname{\mathcal{C}}$ be a simplicial set. Then the construction

$( \mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}) \mapsto (\int _{\operatorname{\mathcal{C}}} \mathscr {F} \rightarrow \operatorname{\mathcal{C}})$

induces a bijection from $\pi _0( \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{QC}})^{\simeq } )$ to the set of equivalence classes of cocartesian fibrations $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ having the following property: for every object $C \in \operatorname{\mathcal{C}}$, the $\infty$-category $\operatorname{\mathcal{E}}_{C} = \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ is essentially small.

Proof of Theorem 5.6.0.2. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibrations of simplicial sets and suppose that, for each vertex $C \in \operatorname{\mathcal{C}}$, the fiber $\operatorname{\mathcal{E}}_{C} = \{ C \} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ is essentially small. We wish to show that $U$ admits a covariant transport representation $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$, which is uniquely determined up to isomorphism (as an object of the functor $\infty$-category $\operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{QC}})$). The existence statement follows by applying Theorem 5.6.2.8 in the special case $\operatorname{\mathcal{C}}_0 = \emptyset$, and the uniqueness follows from Corollary 5.6.2.11. $\square$