$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proposition 8.6.2.3. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of $\infty $-categories. Then the projection map $V: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ of Construction 8.6.2.2 is a cartesian fibration of $\infty $-categories, and the evaluation functor
\[ \operatorname{ev}: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}})\times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{E}}\quad \quad (C, f_ C, u: C \rightarrow C') \mapsto f_ C(u) \]
exhibits $V$ as a cartesian conjugate of $U$.
Proof of Proposition 8.6.2.3.
Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of $\infty $-categories. It follows from Lemma 8.6.2.7 that the projection map $V: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ is a cartesian fibration. We wish to show that the evaluation map
\[ \operatorname{ev}: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}}) \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{E}} \]
exhibits $V$ as a cartesian conjugate of $U$. This follows from Proposition 8.6.2.8, since the identity automorphism of $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}})$ is an equivalence of $\infty $-categories.
$\square$