Kerodon

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

Proposition 8.6.3.5. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets. Then the projection map $V: \operatorname{Cospan}^{\dagger }(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ is a cartesian fibration, which is a cartesian conjugate of $U$.

Proof of Proposition 8.6.3.5. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets. 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.3.11, we see that Construction 8.6.3.9 supplies a commutative diagram

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}^{\dagger } \ar [rr]^-{\Psi } \ar [dr]_{U^{\dagger }} & & \operatorname{Cospan}^{\dagger }(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}) \ar [dl]^{V} \\ & \operatorname{\mathcal{C}}^{\operatorname{op}}, & } \]

where the horizontal map is an equivalence of cartesian fibrations over $\operatorname{\mathcal{C}}^{\operatorname{op}}$. It follows that $V$ is also a cartesian conjugate of $U$. $\square$