# Kerodon

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

Proposition 5.6.7.2 (Extending Cocartesian Fibrations). Let $\operatorname{\mathcal{C}}$ be a simplicial set, let $\operatorname{\mathcal{C}}_0 \subseteq \operatorname{\mathcal{C}}$ be a simplicial subset, and let $U_0: \operatorname{\mathcal{E}}_0 \rightarrow \operatorname{\mathcal{C}}_0$ be a cocartesian fibration of simplicial sets. Suppose that the inclusion $\operatorname{\mathcal{C}}_0 \hookrightarrow \operatorname{\mathcal{C}}$ is a categorical equivalence of simplicial sets. Then there exists a pullback diagram of simplicial sets

$\xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}_0 \ar [r] \ar [d]^{U_0} & \operatorname{\mathcal{E}}\ar [d]^{U} \\ \operatorname{\mathcal{C}}_0 \ar [r] & \operatorname{\mathcal{C}}, }$

where $U$ is a cocartesian fibration.

Proof. By virtue of Theorem 5.6.0.2, there exists a morphism of simplicial sets $\mathscr {F}_0: \operatorname{\mathcal{C}}_0 \rightarrow \operatorname{\mathcal{QC}}$ and an equivalence $G_0: \operatorname{\mathcal{E}}_0 \rightarrow \int _{\operatorname{\mathcal{C}}_0} \mathscr {F}_0$ of cocartesian fibrations over $\operatorname{\mathcal{C}}_0$. Since $\operatorname{\mathcal{QC}}$ is an $\infty$-category (Proposition 5.5.4.3), our assumption that the inclusion $\operatorname{\mathcal{C}}_0 \hookrightarrow \operatorname{\mathcal{C}}$ is a categorical equivalence guarantees that we can extend $\mathscr {F}_0$ to a morphism of simplicial sets $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$. We can then identify $G_0$ with an equivalence $\operatorname{\mathcal{E}}_0 \rightarrow \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \int _{\operatorname{\mathcal{C}}} \mathscr {F}$ of cocartesian fibrations over $\operatorname{\mathcal{C}}_0$. Applying Lemma 5.6.7.1, we can write $U_0$ as the pullback of an inner fibration $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ which is equivalent to the projection map $V: \int _{\operatorname{\mathcal{C}}} \mathscr {F} \rightarrow \operatorname{\mathcal{C}}$ as an inner fibration over $\operatorname{\mathcal{C}}$. Since $V$ is a cocartesian fibration (Proposition 5.6.2.2), it follows that $U$ is also a cocartesian fibration (Proposition 5.1.7.14). $\square$