Kerodon

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

Corollary 5.6.4.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.2.13), Proposition 5.6.4.2 guarantees that $U_0$ is the pullback of a cocartesian fibration $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$. $\square$