Lemma Let $f: Y \rightarrow T$ be a Kan fibration of simplicial sets, and suppose we are given simplicial subsets $X \subseteq Y$ and $S \subseteq T$ satisfying the following conditions:


The morphism $f$ carries $X$ to $S$, and the restriction $f_0 = f|_{X}$ is a Kan fibration from $X$ to $S$.


For every vertex $s \in S$, the inclusion of fibers $X_{s} \hookrightarrow Y_{s}$ is a homotopy equivalence of Kan complexes.

Let $Y' \subseteq Y$ denote the simplicial subset spanned by those simplices $\sigma : \Delta ^{n} \rightarrow Y$ having the property that the restriction $\sigma |_{ S \times _{T} \Delta ^{n} }$ factors through $X$. Then the restriction $f|_{Y'}: Y' \rightarrow T$ is a Kan fibration.

Proof. Set $Y_{S} = S \times _{T} Y \subseteq Y$. It follows from assumption $(b)$ and Corollary that the inclusion $X \hookrightarrow Y_{S}$ is a weak homotopy equivalence, and is therefore anodyne (Corollary Since $f_0$ is a Kan fibration, the lifting problem

\[ \xymatrix { X \ar [r]^-{\operatorname{id}} \ar [d] & X \ar [d]^{f_0} \\ Y_{S} \ar [r]^-{ f|_{Y_ S}} \ar@ {-->}[ur]^{r} & S } \]

admits a solution: that is, there exists a retraction $r$ from $Y_{S}$ to the simplicial subset $X \subseteq Y_{S}$ which is compatible with projection to $S$. Since $f$ is a Kan fibration, Theorem guarantees that the map

\[ \operatorname{Fun}( Y_{S}, Y_ S) \rightarrow \operatorname{Fun}( X, Y_ S) \times _{ \operatorname{Fun}(X,S) } \operatorname{Fun}( Y_{S}, S) \]

is a trivial Kan fibration. We can therefore choose a homotopy $H: \Delta ^{1} \times Y_{S} \rightarrow Y_{S}$ from $\operatorname{id}_{Y_ S} = H|_{ \{ 0\} \times Y_{S} }$ to $r = H|_{ \{ 1\} \times Y_{S} }$, such that $f \circ H$ is the constant homotopy from $f|_{Y_{S}}$ to itself.

Choose an anodyne map of simplicial sets $i: A \hookrightarrow B$. We wish to show that every lifting problem of the form

\[ \xymatrix { A \ar [r]^-{g_0} \ar [d]^{i} & Y' \ar [d]^{ f|_{Y'} } \\ B \ar [r]^-{\overline{g}} \ar@ {-->}[ur]^-{g} & T } \]

admits a solution. Since $f$ is a Kan fibration, we can choose a map $g': B \rightarrow Y$ satisfying $g'|_{A} = g_0$ and $f \circ g = \overline{g}$. Let $B_ S \subseteq B$ denote the simplicial subset given by the fiber product $S \times _{T} B$, and let $g_1: (A \cup B_ S) \rightarrow Y$ be the map of simplicial sets characterized by $g_{1}|_{A} = g_0$ and $g_{1} |_{B_ S} = r \circ g'|_{B_ S}$ (this map is well-defined, since $r \circ g'$ and $g_0$ agree on the intersection $A \cap B_{S}$). Note that $H$ induces a homotopy $h_0: \Delta ^{1} \times (A \cup B_{S} ) \rightarrow Y$ from $g'|_{ A \cup B_{S} }$ to $g_{1}$ (compatible with the projection to $S$). Since $f$ is a Kan fibration, we can lift $h_0$ to a homotopy $h: \Delta ^1 \times B \rightarrow Y$ from $g'$ to some map $g: B \rightarrow Y$, compatible with the projection to $S$ (Remark It follows from the construction that $g$ takes values in the simplicial subset $Y' \subseteq Y$ and satisfies the requirements $g |_{A} = g_0$ and $f \circ g= \overline{g}$. $\square$