$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proposition 4.3.7.6. Let $f: K \rightarrow X$ and $q: X \rightarrow S$ be morphisms of simplicial sets, let $K_0 \subseteq K$ be a simplicial subset, and set $f_0 = f|_{K_0}$. Then:
If $q$ is a right fibration and the inclusion $K_0 \hookrightarrow K$ is anodyne, then the induced map
\[ X_{/f} \rightarrow X_{/f_0} \times _{ S_{ / (q \circ f_0) } } S_{/ (q \circ f)} \]
is a trivial Kan fibration.
If $q$ is a left fibration and the inclusion $K_0 \hookrightarrow K$ is anodyne, then the induced map
\[ X_{f/} \rightarrow X_{f_0/} \times _{ S_{(q \circ f_0)/ } } S_{(q \circ f)/} \]
is a trivial Kan fibration.
Proof.
We will prove the first assertion; the proof of the second is similar. Assume that $q$ is a right fibration and that the inclusion $K_0 \hookrightarrow K$ is anodyne. We wish to show that the map $X_{/f} \rightarrow X_{/f_0} \times _{ S_{ / (q \circ f_0) } } S_{/ (q \circ f)}$ is a trivial Kan fibration. Equivalently, we wish to show that every lifting problem
\[ \xymatrix@C =50pt@R=50pt{ A \ar [r] \ar [d] & X_{/f} \ar [d] \\ A' \ar [r] \ar@ {-->}[ur] & X_{/f_0} \times _{ S_{ / (q \circ f_0) } } S_{/ (q \circ f)} } \]
admits a solution, provided that the left vertical map $A \rightarrow A'$ is a monomorphism. Unwinding the definitions, we see that this can be rephrased as a lifting problem
\[ \xymatrix@C =50pt@R=50pt{ (A \star K) \coprod _{ (A \star K_0) } (A' \star K_0) \ar [r] \ar [d] & X \ar [d]^{q} \\ A' \star K \ar [r] \ar@ {-->}[ur] & S. } \]
This problem admits a solution, since the vertical map on the left is right anodyne (Proposition 4.3.7.1) and $q$ is a right fibration.
$\square$