Kerodon

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

Corollary 4.3.7.19. Let $X$ be a contractible 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 trivial Kan fibrations. In particular, $X_{/f}$ and $X_{f/}$ are also contractible Kan complexes.

Proof. Apply Corollary 4.3.7.16 in the special case $S = \Delta ^{0}$ (or Corollary 4.3.7.18 in the special case $K_0 = \emptyset $). $\square$