Lemma 14.30.8. Let $f : X \to Y$ be a trivial Kan fibration of simplicial sets. Then $f$ is a homotopy equivalence.

Proof. By Lemma 14.30.2 we can choose an right inverse $g : Y \to X$ to $f$. Consider the diagram

$\xymatrix{ \partial \Delta [1] \times X \ar[d] \ar[r] & X \ar[d] \\ \Delta [1] \times X \ar[r] \ar@{-->}[ru] & Y }$

Here the top horizontal arrow is given by $\text{id}_ X$ and $g \circ f$ where we use that $(\partial \Delta [1] \times X)_ n = X_ n \amalg X_ n$ for all $n \geq 0$. The bottom horizontal arrow is given by the map $\Delta [1] \to \Delta [0]$ and $f : X \to Y$. The diagram commutes as $f \circ g \circ f = f$. By Lemma 14.30.2 we can fill in the dotted arrow and we win. $\square$

In your comment you can use Markdown and LaTeX style mathematics (enclose it like $\pi$). A preview option is available if you wish to see how it works out (just click on the eye in the toolbar).