Corollary 4.3.7.5. Let $X$ be a Kan complex and let $f: K \rightarrow X$ be a morphism of simplicial sets. Then the projection maps
\[ X_{/f} \rightarrow X \quad \quad X_{f/} \rightarrow X \]
are Kan fibrations. In particular, the simplicial sets $X_{/f}$ and $X_{f/}$ are Kan complexes.