A fibration $p : E \rightarrow X$ is trivial iff $p$ is a homotopy equivalence

Question

My question concerns propositions 3.2.5 and 3.2.6 of Joyal and Tierney's lecture notes on simplicial homotopy theory.

My primary problem is with the beginning of the proof of the latter proposition. It is supposed that there exists a filler $k'$ of the given diagram, but I do not understand why it should. I have three ideas:

1. The inclusion $X \times (0) \rightarrow X \times I$ is anodyne. I don't see why it should be, while I do understand that $(0) \rightarrow I$ is a horn inclusion.
2. The covering homotopy extension property (Proposition 3.2.2) is used. For this we would need a monomorphism $E \rightarrow X$, which I don't know we have.
3. We are pretending that we have already solved the problem, which means that $p$ is trivial and thus such a filler exists by the fact that $X \times (0) \rightarrow I$ is monic.

Even taking this for granted, I do not see why it follows that we may assume that $ps = id_X$. Clearly $ps' = id_X$, but why would that also hold for $ps$?

Answer 1

Your first point follows from Corollary 3.2.1: the morphism $p : E \to X$ is a fibration, hence the induced morphism $p^X : E^X \to X^X$ is a fibration. Finding a lift as in the proof amounts to finding a lift in the following commutative square: $$\require{AMScd} \begin{CD} (0) @>>> E^X \\ @VVV @VVV \\ I @>>> X^X \end{CD},$$ which exists because the right vertical map is anodyne and the left vertical map is a fibration. (PS: this shows that $X \times (0) \to X \times I$ is anodyne for all $X$. This fact is spelled out at the top of page 45.)

For your second point: it's not necessarily true that $ps = \operatorname{id}_X$. What the authors are saying is that instead of choosing $s$ in the beginning, you could have chosen $s'$. So to avoid carrying a $'$ everywhere they will henceforth use the name $s$ for what was called $s'$, and forget about the old $s$ altogether.