# Kerodon

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

Proposition 3.1.6.10. Let $f: X_{} \rightarrow S_{}$ be a trivial Kan fibration of simplicial sets. Then $f$ is a homotopy equivalence.

Proof. Since $f$ is a trivial Kan fibration, the lifting problem

$\xymatrix@R =50pt@C=50pt{ \emptyset \ar [r] \ar [d] & X_{} \ar [d]^{f} \\ S_{} \ar [r]^-{\operatorname{id}} \ar@ {-->}[ur] & S_{} }$

admits a solution (Proposition 1.4.5.3). We can therefore choose a morphism of simplicial sets $g: S_{} \rightarrow X_{}$ which is a section of $f$: that is, $f \circ g$ is the identity morphism from $S_{}$ to itself. We will complete the proof by showing that $g$ is a homotopy inverse to $f$. In fact, we claim that there exists a homotopy $h$ from $\operatorname{id}_{X_{}}$ to the composition $g \circ f$. This follows from the solvability of the lifting problem

$\xymatrix@C =100pt{ \{ 0,1\} \times X_{} \ar [r]^-{(\operatorname{id}, g \circ f)} \ar [d] & X_{} \ar [d]^{f} \\ \Delta ^1 \times X_{} \ar [r]^-{f} \ar@ {-->}[ur]^-{h} & S_{}. }$
$\square$