Theorem 3.3.8.1. Let $f: X \rightarrow S$ be a Kan fibration between simplicial sets, and let $g: S \hookrightarrow S'$ be an anodyne map. Then there exists a pullback diagram of simplicial sets
where $f'$ is a Kan fibration.
Proof of Theorem 3.3.8.1. Let $f: X \rightarrow S$ be a Kan fibration of simplicial sets. Let us abuse notation by identifying $X$ and $S$ with simplicial subsets of $Y = \operatorname{Ex}^{\infty }(X)$ and $T = \operatorname{Ex}^{\infty }(S)$, respectively (via the monomorphisms $\rho _{X}^{\infty }: X \hookrightarrow \operatorname{Ex}^{\infty }(X)$ and $\rho _{S}^{\infty }: S \hookrightarrow \operatorname{Ex}^{\infty }(S)$), and let $Y' \subseteq \operatorname{Ex}^{\infty }(X)$ be the simplicial subset defined in the statement of Lemma 3.3.8.4. Let $g: S \hookrightarrow S'$ be an anodyne morphism of simplicial sets. Since $\operatorname{Ex}^{\infty }(S)$ is a Kan complex (Proposition 3.3.6.9), the morphism $\rho ^{\infty }_{S}: S \rightarrow \operatorname{Ex}^{\infty }(S)$ extends to a map of simplicial sets $u: S' \rightarrow \operatorname{Ex}^{\infty }(S)$. Set $X' = S' \times _{ \operatorname{Ex}^{\infty }(S)} Y'$, so that we have a commutative diagram
where the right square and outer rectangle are pullback diagrams, so the left square is a pullback diagram as well. Since the projection map $Y' \rightarrow \operatorname{Ex}^{\infty }(S)$ is a Kan fibration (Lemma 3.3.8.4), it follows that $f'$ is also a Kan fibration. $\square$