# Kerodon

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

Corollary 5.7.7.3. Let $U_0: \operatorname{\mathcal{E}}_0 \rightarrow \operatorname{\mathcal{C}}_0$ be a cocartesian fibration of simplicial sets. Then there exists a pullback diagram

$\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]^-{F} & \operatorname{\mathcal{C}}, }$

where $U$ is a cocartesian fibration of $\infty$-categories and $F$ is inner anodyne.

Proof. Using Corollary 4.1.3.3, we can choose an inner anodyne map $F: \operatorname{\mathcal{C}}_0 \hookrightarrow \operatorname{\mathcal{C}}$, where $\operatorname{\mathcal{C}}$ is an $\infty$-category. Since $F$ is a categorical equivalence of simplicial sets (Corollary 4.5.3.14), Proposition 5.7.7.2 guarantees that $U_0$ is the pullback of a cocartesian fibration $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$. $\square$