Kerodon

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

Proposition 1.4.7.6. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $f: X_{\bullet } \hookrightarrow Y_{\bullet }$ be an inner anodyne morphism of simplicial sets. Then the induced map $p: \operatorname{Fun}( Y_{\bullet }, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}( X_{\bullet }, \operatorname{\mathcal{C}})$ is a trivial Kan fibration.

Proof. To show that $p$ is a trivial Kan fibration, it will suffice to show that it has the right lifting property with respect to every monomorphism of simplicial sets $f': X'_{\bullet } \hookrightarrow Y'_{\bullet }$. This is equivalent to the assertion that every map of simplicial sets

\[ g_0: (Y_{\bullet } \times X'_{\bullet } ) \coprod _{ (X_{\bullet } \times X'_{\bullet })} (X_{\bullet } \times Y'_{\bullet } ) \rightarrow \operatorname{\mathcal{C}} \]

can be extended to a map $g: Y_{\bullet } \times Y'_{\bullet } \rightarrow \operatorname{\mathcal{C}}$. This follows from Proposition 1.4.6.7, since $\operatorname{\mathcal{C}}$ is an $\infty $-category and the map

\[ u_{f,f'}: (Y_{\bullet } \times X'_{\bullet } ) \coprod _{ (X_{\bullet } \times X'_{\bullet })} (X_{\bullet } \times Y'_{\bullet } ) \hookrightarrow Y_{\bullet } \times Y'_{\bullet } \]

is inner anodyne (Lemma 1.4.7.5). $\square$