# Kerodon

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

Remark 5.1.2.5. Assuming Theorem 5.1.2.2, one can give a more direct proof of Lemma 5.1.2.4. Let $q: X \rightarrow S$ be a left fibration of simplicial sets, where $S$ is a Kan complex. To show that $q$ is a Kan fibration, it will suffice (by virtue of Theorem 5.1.2.2) to show that the covariant transport functor $\mathrm{h} \mathit{S} \rightarrow \mathrm{h} \mathit{\operatorname{Kan}}$ carries every morphism in $\mathrm{h} \mathit{S}$ to an invertible morphism in $\mathrm{h} \mathit{\operatorname{Kan}}$. This is clear, since the homotopy category $\mathrm{h} \mathit{S}$ is a groupoid (Proposition 1.3.6.11).