$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proposition 4.3.6.8. Let $q: X \rightarrow S$ be an inner fibration of simplicial sets, let $f: K \rightarrow X$ be any morphism of simplicial sets, let $K_0$ be a simplicial subset of $K$, and set $f_0 = f|_{ K_0}$. Then the restriction map
\[ X_{/f} \rightarrow X_{/f_0} \times _{ S_{ / (q \circ f_0)}} S_{ / (q \circ f)} \]
is a right fibration, and the restriction map
\[ X_{f/} \rightarrow X_{f_0/} \times _{ S_{(q \circ f_0)/}} S_{(q \circ f)/} \]
is a left fibration.
Proof.
We will prove the first assertion; the second follows by a similar argument. By virtue of Proposition 4.2.4.5, it will suffice to show that for every right anodyne morphism $i: A \hookrightarrow A'$, every lifting problem
\[ \xymatrix@R =50pt@C=50pt{ A \ar [d]^{i} \ar [r] & X_{/f} \ar [d] \\ A' \ar [r] \ar@ {-->}[ur] \ar [r] & X_{/f_0} \times _{ S_{ / (q \circ f_0)}} S_{ / (q \circ f)} } \]
admits a solution. Unwinding the definitions, this is equivalent to solving an associated lifting problem
\[ \xymatrix@R =50pt@C=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@ {-->}[ur] \ar [r] & S, } \]
where the left vertical morphism is the pushout-join of Construction 4.3.6.3. Proposition 4.3.6.4 guarantees that this morphism is inner anodyne, so that the desired extension exists by virtue of our assumption that $q$ is an inner fibration (Proposition 4.1.3.1).
$\square$