Kerodon

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

Theorem 8.6.4.1. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets. Then $U$ admits a cocartesian dual $U^{\vee }: \operatorname{\mathcal{E}}^{\vee } \rightarrow \operatorname{\mathcal{C}}$, which is uniquely determined up to equivalence.

Proof of Theorem 8.6.4.1. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets. Fix an uncountable cardinal $\kappa $ such that $U$ is locally $\kappa $-small. Proposition 8.6.4.8 implies that the projection map $\pi ^{\operatorname{corep}}: \operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa }) \rightarrow \operatorname{\mathcal{C}}$ is a cocartesian dual of $U$, and Proposition 8.6.4.18 implies that any other cocartesian dual $U^{\vee }: \operatorname{\mathcal{E}}^{\vee } \rightarrow \operatorname{\mathcal{C}}$ is equivalent to $\pi ^{\operatorname{corep}}$. $\square$