$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proposition 5.1.4.18. 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:
- $(1)$
The induced map $q': X_{/f} \rightarrow S_{/(q \circ f)}$ is a cartesian fibration of simplicial sets.
- $(2)$
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
\[ X_{/f} \xrightarrow {u} X \times _{S} S_{/(q \circ f)} \xrightarrow {v} S_{ /(q \circ f)}. \]
Since $q$ is an inner fibration, the morphism $u$ is a right fibration (Proposition 4.3.6.8). In particular, $u$ is a cartesian fibration and every edge of $X_{/f}$ is $u$-cartesian (Proposition 5.1.4.15). The morphism $v$ is a pullback of $q$, and is therefore a cartesian fibration (Remark 5.1.4.6). Moreover, an edge of $X \times _{S} S_{/(q \circ f)}$ is $v$-cartesian if and only if its image in $X$ is $q$-cartesian. Assertions $(1)$ and $(2)$ now follow from Proposition 5.1.4.14.
$\square$