Kerodon

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

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 essentially small cocartesian fibrations $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$.

Proof of Theorem 5.6.0.2. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be an essentially small cocartesian fibrations of simplicial sets. 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.5.10 in the special case $\operatorname{\mathcal{C}}_0 = \emptyset $, and the uniqueness follows from Corollary 5.6.5.13. $\square$