Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

Corollary 5.1.2.5. Let $q: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be an inner fibration of $\infty $-categories, and let $f: X \rightarrow Y$ and $f': X' \rightarrow Y'$ be morphisms of $\operatorname{\mathcal{C}}$ which are isomorphic as objects of the $\infty $-category $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}})$. Then $f$ is $q$-cartesian if and only if $f'$ is $q$-cartesian. Similarly, $f$ is $q$-cocartesian if and only if $f'$ is $q$-cocartesian.

Proof. Our assumption that $f$ is isomorphic to $f'$ in $\operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}})$ guarantees that there exists a commutative diagram

\[ \xymatrix@R =50pt@C=50pt{ X \ar [d]^-{e} \ar [r]^-{f} & Y \ar [d]^-{e'} \\ X' \ar [r]^-{f'} & Y', } \]

where $e$ and $e'$ are isomorphisms (and therefore $q$-cartesian by virtue of Proposition 5.1.1.9). The desired result now follows from Corollary 5.1.2.4. $\square$