Kerodon

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

Corollary 8.6.3.14 (Uniqueness). Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets. Then $U$ admits a cartesian conjugate, which is uniquely determined up equivalence.

Proof. Combining Propositions 8.6.3.11 and 8.6.3.5, we see that a cartesian fibration $U^{\dagger }: \operatorname{\mathcal{E}}^{\dagger } \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ is conjugate to $U$ if and only if it is equivalent to the projection map $\operatorname{Cospan}^{\dagger }( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$. $\square$