Kerodon

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

Remark 8.1.9.3. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of $\infty $-categories and let $W$ be the collection of all $U$-cocartesian morphisms of $\operatorname{\mathcal{E}}$. Then we have a commutative diagram

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [r] \ar [d]^{U} & \operatorname{Cospan}^{\mathrm{all}, \mathrm{iso}}(\operatorname{\mathcal{E}}) \ar [r] \ar [d] & \operatorname{Cospan}^{ \mathrm{all},W}( \operatorname{\mathcal{E}}) \ar [d] \\ \operatorname{\mathcal{C}}\ar [r] & \operatorname{Cospan}^{\mathrm{all}, \mathrm{iso}}( \operatorname{\mathcal{C}}) \ar [r] & \operatorname{Cospan}( \operatorname{\mathcal{C}}), } \]

where the horizontal maps on the left are equivalences of $\infty $-categories (Proposition 8.1.7.6), and the right half of the diagram is a pullback square (Proposition 5.1.1.9). It follows that from Proposition 8.1.9.1 that map $\operatorname{Cospan}^{\mathrm{all}, \mathrm{iso}}(\operatorname{\mathcal{E}}) \rightarrow \operatorname{Cospan}^{\mathrm{all}, \mathrm{iso}}( \operatorname{\mathcal{C}})$ is an inner fibration of $\infty $-categories. In fact, it is even an isofibration: this follows easily from the description of isomorphisms in the $\infty $-categories $\operatorname{Cospan}^{\mathrm{all}, \mathrm{iso}}(\operatorname{\mathcal{C}})$ and $\operatorname{Cospan}^{\mathrm{all}, \mathrm{iso}}(\operatorname{\mathcal{E}})$ supplied by Corollary 8.1.6.10 (together with the fact that $U$ is an isofibration; see Proposition 5.1.4.9). Applying Theorem 5.1.6.1 to the right side of the diagram, we conclude that the map $\operatorname{Cospan}^{\mathrm{all}, \mathrm{iso}}(\operatorname{\mathcal{E}}) \rightarrow \operatorname{Cospan}^{\mathrm{all}, \mathrm{iso}}(\operatorname{\mathcal{C}})$ is also a cocartesian fibration of simplicial sets. Moreover, Corollary 4.5.2.29 guarantees that the induced map

\[ \operatorname{\mathcal{E}}\hookrightarrow \operatorname{\mathcal{C}}\times _{ \operatorname{Cospan}^{\mathrm{all}, \mathrm{iso}}(\operatorname{\mathcal{C}}) } \operatorname{Cospan}^{\mathrm{all}, \mathrm{iso}}(\operatorname{\mathcal{E}}) \simeq \operatorname{\mathcal{C}}\times _{ \operatorname{Cospan}(\operatorname{\mathcal{C}}) } \operatorname{Cospan}^{\mathrm{all},W}(\operatorname{\mathcal{E}}) \]

is an equivalence of $\infty $-categories.