Proposition 5.1.4.20. Let $q: X \rightarrow S$ be a cartesian fibration of simplicial sets and let $f: K \rightarrow X$ be any morphism of simplicial sets. Then:
The induced map $q': X_{f/} \rightarrow S_{(q \circ f)/}$ is a cartesian fibration of simplicial sets.
An edge $e$ of $X_{f/}$ is $q'$-cartesian if and only if its image in $X$ is $q$-cartesian.
Proof. The morphism $q'$ factors as a composition
where $v$ is a pullback of $q$ and is therefore a cartesian fibration by virtue of Remark 5.1.4.6. The morphism $u$ is a left fibration (Proposition 4.3.6.8), and therefore an inner fibration. It follows that $q'$ is an inner fibration (Remark 4.1.1.8).
Let us say that an edge $e$ of $X_{f/}$ is special if its image in $X$ is $q$-cartesian. If this condition is satisfied, then $u(e)$ is $v$-cartesian (Remark 5.1.4.6) and $e$ is $u$-cartesian (Lemma 5.1.4.19), so that $e$ is $q'$-cartesian by virtue of Remark 5.1.1.6. This proves the “if” direction of assertion $(2)$.
To prove $(1)$, it will suffice to show that for every vertex $y$ of the simplicial set $X_{f/}$ and every edge $\overline{e}: \overline{x} \rightarrow q'(y)$ of the simplicial set $S_{ (q \circ f)/}$, there exists a special edge $e: x \rightarrow y$ of $X_{f/}$ satisfying $q'(e) = \overline{e}$. Since $v$ is a cartesian fibration, we can choose a $v$-cartesian edge $\widetilde{e}: \widetilde{x} \rightarrow u(y)$ of the simplicial set $X \times _{S} S_{(q \circ f)/}$. In this case, the image $\widetilde{e}$ in $X$ is $q$-cartesian (Remark 5.1.4.6). Corollary 5.1.1.16 then guarantees that there exists an edge $e: x \rightarrow y$ of $X_{f/}$ satisfying $u(e) = \widetilde{e}$. The edge $e$ is automatically special and satisfies $q'(e) = (v \circ u)(e) = v( \widetilde{e} ) = \overline{e}$, as desired.
To complete the proof of $(2)$, it will suffice to show that every $q'$-cartesian edge $e: x \rightarrow z$ of $X_{f/}$ is special. It follows from the preceding argument that there exists a special edge $e': y \rightarrow z$ satisfying $q'(e') = q'(e)$, which is also $q'$-cartesian. Applying Remark 5.1.3.8, we can choose a $2$-simplex $\sigma $ of $X_{f/}$ as indicated in the diagram
where $e''$ is an isomorphism in the $\infty $-category $\{ q'(x) \} \times _{ S_{ (q \circ f)/} } X_{f/}$. Using Proposition 5.1.4.12, we deduce that the image of $e''$ in $X$ is $q$-cartesian. Applying Proposition 5.1.4.13, we conclude the image of $e$ in $X$ is also $q$-cartesian, as desired. $\square$