Corollary 4.3.7.4. 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, 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 Kan fibrations.