Kerodon

Remark 11.6.0.223. Assuming Theorem 5.2.2.20, one can give a more direct proof of ***. 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.2.2.20) to show that the covariant transport functor $\operatorname {h}\! \mathit{S} \rightarrow \operatorname {h}\! \mathit{\operatorname{Kan}}$ carries every morphism in $\operatorname {h}\! \mathit{S}$ to an invertible morphism in $\operatorname {h}\! \mathit{\operatorname{Kan}}$. This is clear, since the homotopy category $\operatorname {h}\! \mathit{S}$ is a groupoid (Proposition 1.4.6.10).