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

Corollary Let $f: X \rightarrow S$ be a Kan fibration between Kan complexes. The following conditions are equivalent:


The morphism $f$ is a trivial Kan fibration.


The morphism $f$ is a homotopy equivalence.


The map $f$ induces a bijection $\pi _0(f): \pi _0(X) \rightarrow \pi _0(S)$. Moreover, for each vertex $x \in X$ having image $s = f(x)$ in $S$, the induced map $\pi _{n}(f): \pi _{n}(X,x) \rightarrow \pi _{n}(S,s)$ is an isomorphism for $n > 0$.


For each vertex $s \in S$, the fiber $X_{s}$ is connected. Moreover, the homotopy groups $\pi _{n}(X_ s, x)$ vanish for each vertex $x \in X_{s}$ and each $n > 0$.

Proof. The implication $(1) \Rightarrow (2)$ follows from Proposition, the implication $(2) \Rightarrow (3)$ from Corollary, and the implication $(4) \Rightarrow (1)$ from Proposition The implication $(3) \Rightarrow (4)$ follows from the long exact sequence of Theorem $\square$