# Kerodon

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

Theorem 3.3.0.1. 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:

$(a)$

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

$(b)$

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

$(c)$

The morphism $f'$ is a Kan fibration.

$(d)$

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