Kerodon

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

Corollary 11.10.1.16. Let $q: X \rightarrow S$ and $q: X' \rightarrow S$ be morphisms of simplicial sets which are both cartesian fibrations and cocartesian fibrations. Then $q$ and $q'$ are equivalent as cartesian fibrations over $S$ if and only if they are equivalent as cocartesian fibrations over $S$.