# Kerodon

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

Theorem 8.6.5.6. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets. Then the projection map $\operatorname{Cospan}^{\operatorname{CCart}}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}$ is also a cocartesian fibration, which is a cocartesian dual of $U$.

Proof of Theorem 8.6.5.6 from Proposition 8.6.5.12. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets and let $U^{\vee }: \operatorname{Cospan}^{\operatorname{CCart}}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}$ be the projection map; we wish to show that $U^{\vee }$ is a cocartesian dual of $U$. Using Corollary 5.6.7.3, we can choose a pullback diagram

$\xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [d]^{U} \ar [r] & \operatorname{\mathcal{E}}' \ar [d]^{U'} \\ \operatorname{\mathcal{C}}\ar [r] & \operatorname{\mathcal{C}}', }$

where $U'$ is a cocartesian fibration of $\infty$-categories. Using Remarks 8.6.3.4 and 8.6.5.4, we can replace $U$ by $U'$ and thereby reduce to the case where $\operatorname{\mathcal{C}}$ is an $\infty$-category. In this case, we have commutative diagrams

$\xymatrix@R =50pt@C=50pt{ \operatorname{Cospan}^{\operatorname{CCart}}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}) \ar [d]^{U^{\vee }} \ar [r] & \operatorname{Cospan}^{L,R}(\operatorname{\mathcal{E}}) \ar [d]^{V_{-}} & \operatorname{\mathcal{E}}\ar [d]^{U} \ar [r] & \operatorname{Cospan}^{\mathrm{all}, \mathrm{iso}}(\operatorname{\mathcal{E}}) \ar [d]^{ V_{+} } \\ \operatorname{\mathcal{C}}\ar [r] & \operatorname{Cospan}^{\mathrm{all}, \mathrm{iso} }(\operatorname{\mathcal{C}}) & \operatorname{\mathcal{C}}\ar [r] & \operatorname{Cospan}^{\mathrm{all}, \mathrm{iso}}(\operatorname{\mathcal{C}}), }$

where the vertical maps are cocartesian fibrations, the diagram on the left is a pullback square, and the diagram on the right is a categorial pullback square (the horizontal maps are equivalences of $\infty$-categories by virtue of Proposition 8.1.7.6). Using Remark 8.6.3.4 again, we are reduced to showing that $V_{-}$ is a cocartesian dual of $V_{+}$, which follows from Proposition 8.6.5.12. $\square$