Remark Assuming Theorem, one can give a more direct proof of Lemma 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 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