Corollary 4.3.7.7. Let $X$ be a Kan complex, let $f: K \rightarrow X$ be a morphism of simplicial sets, let $K_0 \subseteq K$ be a simplicial subset for which the inclusion $K_0 \hookrightarrow K$ is anodyne, 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.