Kerodon

Proof of Proposition 8.6.6.1. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ and $U^{\vee }: \operatorname{\mathcal{E}}^{\vee } \rightarrow \operatorname{\mathcal{C}}$ be cocartesian fibrations of simplicial sets. Fix an uncountable cardinal $\kappa $ such that $U$ and $U^{\vee }$ are locally $\kappa $-small. If $U$ is a cocartesian dual of $U^{\vee }$, then Proposition 8.6.5.18 guarantees that $U^{\vee }$ is equivalent to the cocartesian fibration $\pi ^{\operatorname{corep}}: \operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}^{< \kappa } ) \rightarrow \operatorname{\mathcal{C}}$. Combining this observation with Theorem 8.6.6.15, we conclude that $U^{\operatorname{op}}$ is a cartesian conjugate of $U^{\vee }$.

We now prove the converse. Assume that $U^{\operatorname{op}}$ is a cartesian conjugate of $U^{\vee }$; we wish to show that $U$ is a cartesian dual of $U^{\vee }$. Applying Theorem 8.6.5.1, we see that $U^{\vee }$ admits a cocartesian dual $U': \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}$. The first part of the proof shows that the opposite fibration $U'^{\operatorname{op}}: \operatorname{\mathcal{E}}'^{\operatorname{op}} \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ is a cartesian conjugate of $U^{\vee }$, and is therefore equivalent to the cartesian fibration $U^{\operatorname{op}}$ (Corollary 8.6.3.14). It follows that the cocartesian fibrations $U$ and $U'$ are also equivalent, so that $U$ is also a cocartesian dual of $U^{\vee }$. $\square$