Theorem Let $f: X \rightarrow S$ be a Kan fibration of simplicial sets. Then there exists a commutative diagram of simplicial sets

\[ \xymatrix { X \ar [r]^-{g'} \ar [d]^{f} & X' \ar [d]^{f'} \\ S \ar [r]^-{g} & S' } \]

with the following properties:


The simplicial sets $S'$ and $X'$ are Kan complexes.


The morphisms $g$ and $g'$ are weak homotopy equivalences.


The morphism $f'$ is a Kan fibration.


For every vertex $s \in S$, the induced map $g'_{s}: X_{s} \rightarrow X'_{ g(s)}$ is a homotopy equivalence of Kan complexes.