Kerodon

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

Proof. Using Corollary 8.6.2.4, we can choose a cartesian fibration $U^{\dagger }: \operatorname{\mathcal{E}}^{\dagger } \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ and a morphism $T: \operatorname{\mathcal{E}}^{\dagger } \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{E}}$ which exhibits $U^{\dagger }$ as a cartesian conjugate of $U$. Applying Proposition 8.6.6.6, we see that the comparison map of Construction 8.6.6.4 provides a morphism $\operatorname{\mathcal{E}}^{\dagger } \rightarrow \operatorname{Cospan}^{\operatorname{CCart}}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}})^{\operatorname{op}}$ which is an equivalence of cartesian fibrations over $\operatorname{\mathcal{C}}^{\operatorname{op}}$. It follows that the projection map $\operatorname{Cospan}^{\operatorname{CCart}}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}})^{\operatorname{op}} \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ is also a cartesian conjugate of $U$. $\square$