Kerodon

Proof of Proposition 11.9.1.9. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of $\infty $-categories, and let

be the left fibration of Lemma 11.9.1.11. We wish to show that the left fibraiton $V$ exhibits $V_{-}: \operatorname{Cospan}^{L,R}(\operatorname{\mathcal{E}}) \rightarrow \operatorname{Cospan}^{ \mathrm{all}, \mathrm{iso}}(\operatorname{\mathcal{C}})$ as a cocartesian dual of $V_{+}: \operatorname{Cospan}^{\mathrm{all}, \mathrm{iso}}( \operatorname{\mathcal{E}}) \rightarrow \operatorname{Cospan}^{ \mathrm{all}, \mathrm{iso}}(\operatorname{\mathcal{C}})$. For each object $C \in \operatorname{\mathcal{C}}$, let $\operatorname{\mathcal{E}}_{C} = \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ denote the corresponding fiber of $U$. Then we have a canonical isomorphism

where $\widetilde{L}_{C}$ denotes the collection of all morphisms of $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{E}}_{C} )$ for which the image in $\operatorname{Fun}( \{ 0\} , \operatorname{\mathcal{E}}_{C} )$ is an isomorphism, and $\widetilde{R}_{C}$ denotes the collection of morphisms $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{E}}_{C} )$ for which the image in $\operatorname{Fun}( \{ 1\} , \operatorname{\mathcal{E}}_{C} )$ is an isomorphism. The left fibration $V$ then restricts to a coupling of $\infty $-categories

which is balanced by virtue of Proposition 11.9.1.1. Moreover, if $f$ is an object of the $\infty $-category $\operatorname{Cospan}^{ \widetilde{L}, \widetilde{R} }( \operatorname{Fun}( \operatorname{\mathcal{C}}\times \Delta ^1 / \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) )$ satisfying $V(f) = C$, then $f$ is universal (with respect to the coupling $V_{C}$) if and only if it is an isomorphism when regarded as a morphism in the $\infty $-category $\operatorname{\mathcal{E}}_{C}$ (Corollary 11.9.1.6).

Let $u: f \rightarrow g$ be a morphism in the $\infty $-category $\operatorname{Cospan}^{ \widetilde{L}, \widetilde{R} }( \operatorname{Fun}( \operatorname{\mathcal{C}}\times \Delta ^1 / \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) )$, having image $\overline{u}: C \rightarrow D$ in the $\infty $-category $\operatorname{Cospan}^{ \mathrm{all}, \mathrm{iso}}(\operatorname{\mathcal{C}})$. Assume that the image of $u$ in $\operatorname{Cospan}^{L,R}(\operatorname{\mathcal{E}})$ is $V_{-}$-cocartesian and that the image of $u$ in $\operatorname{Cospan}^{\mathrm{all}, \mathrm{iso}}(\operatorname{\mathcal{E}})$ is $V_{+}$-cocartesian. To complete the proof, we must show that if $f$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{E}}_{C}$, then $g$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{E}}_{D}$. To prove this, let us identify $u$ with a commutative diagram

in the $\infty $-category $\operatorname{\mathcal{E}}$, where $s_{-}$ is $U$-cocartesian and $t_{+}$ is an isomorphism. Since the image of $u$ in $\operatorname{Cospan}^{ \mathrm{all}, \mathrm{iso} }(\operatorname{\mathcal{E}})$ is $V_{+}$-cocartesian, the morphism $s_{+}$ is $U$-cocartesian. Applying Corollary 5.1.2.4, we deduce that the morphism $h$ is $U$-cocartesian. Since the image of $u$ in $\operatorname{Cospan}^{ L,R}(\operatorname{\mathcal{E}})$ is $V_{-}$-cocartesian, the morphism $t_{-}$ is an isomorphism. Applying Corollary 5.1.2.5, we deduce that $g$ is $U$-cocartesian when regarded as a morphism of $\operatorname{\mathcal{E}}$, and is therefore an isomorphism in the $\infty $-category $\operatorname{\mathcal{E}}_{D}$ (Example 5.1.3.6). $\square$