# Kerodon

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

Corollary 5.6.3.14 (The Universal Left Fibration). For every simplicial set $\operatorname{\mathcal{C}}$, the construction

$\mathscr {F} \mapsto \int _{\operatorname{\mathcal{C}}} \mathscr {F} = \operatorname{\mathcal{C}}\times _{ \operatorname{\mathcal{S}}} \operatorname{\mathcal{S}}_{\ast }$

induces a bijection from $\pi _0( \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}})^{\simeq } )$ to the set of equivalence classes of left fibrations $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ having essentially small fibers.

Proof. Combine Theorem 5.6.3.6 (applied to the full subcategory $\operatorname{\mathcal{S}}\subset \operatorname{\mathcal{QC}}$) with with Proposition 5.1.4.14. $\square$