Kerodon

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

Corollary 4.3.7.18. Let $X$ be a contractible Kan complex, let $f: K \rightarrow X$ be a morphism of simplicial sets, let $K_0$ be a simplicial subset of $K$, and set $f_0 = f|_{K_0}$. Then the restriction maps

\[ X_{/f} \rightarrow X_{/f_0} \quad \quad X_{f/} \rightarrow X_{f_0/} \]

are trivial Kan fibrations.

Proof. Apply Proposition 4.3.7.15 in the special case $S = \Delta ^{0}$. $\square$