Kerodon

Corollary 8.6.6.2 (Symmetry). Let $\operatorname{\mathcal{C}}$ be a simplicial set, let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration, and let $U^{\dagger }: \operatorname{\mathcal{E}}^{\dagger } \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ be a cartesian fibration. Then $U^{\dagger }$ is a cartesian conjugate of $U$ if and only if $U^{\operatorname{op}}$ is a cartesian conjugate of $U^{\dagger , \operatorname{op}}$.