Kerodon

Proof. It follows from Proposition 8.1.7.6 that the inclusion maps

are equivalences of $\infty $-categories. By virtue of Corollary 5.1.7.16, it will suffice to show that for every pair of objects $X,Y \in \operatorname{\mathcal{C}}$, the morphism $\Xi $ induces a homotopy equivalence of Kan complexes

We complete the proof by observing that $\Xi _{X,Y}$ fits into a commutative diagram of Kan complexes

where the left vertical map is the homotopy equivalence of Corollary 8.1.2.10, the right vertical map is the homotopy equivalence of Example 8.1.7.7, and the upper horizontal map is the homotopy equivalence of Proposition 4.6.5.10. $\square$

Proof. Let us abuse notation further by identifying $f$ with an object of the twisted arrow $\infty $-category $\operatorname{Tw}(\operatorname{\mathcal{C}})$, so that the comparison functor $\Xi : \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{Cospan}^{L,R}( \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}}) )$ of Construction 11.9.1.3 satisfies $\Xi (f) = f$ (Remark 11.9.1.4). By virtue of Proposition 11.9.1.5 and Remark 8.3.2.8, we are reduced to showing that $f$ is an isomorphism if and only if it is universal with respect to the twisted arrow coupling $\operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}} \times \operatorname{\mathcal{C}}$, which follows from Example 8.2.1.5. $\square$

Proof of Theorem 11.9.1.12 from Proposition 11.9.1.9. 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

where $U'$ is a cocartesian fibration of $\infty $-categories. Using Remarks 8.6.4.4 and 8.6.3.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

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.4.4 again, we are reduced to showing that $V_{-}$ is a cocartesian dual of $V_{+}$, which follows from Proposition 11.9.1.9. $\square$

Proof. Let $\pi : \operatorname{\mathcal{E}}\times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{E}}$ denote the functor given by projection onto the second factor. Let $L'$ denote the collection of all $\pi $-cocartesian morphisms of $\operatorname{\mathcal{E}}\times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$: that is, morphisms $(u,v)$ where $u$ is a $U$-cocartesian morphism in $\operatorname{\mathcal{E}}$. Let $R'$ denote the collection of all morphisms $(u,v)$ of $\operatorname{\mathcal{E}}\times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ where $v$ is an isomorphism in $\operatorname{\mathcal{E}}$. It follows from Proposition 8.1.9.10 (and Example 8.1.6.6) that the pair $(L',R')$ is pushout-compatible, in the sense of Definition 8.1.6.5. Moreover, we have a canonical isomorphism of simplicial sets

Using Lemma 8.6.3.6, we see that $\pi $ induces a cocartesian fibration $\operatorname{Cospan}^{L',R'}(\operatorname{\mathcal{E}}\times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}) \rightarrow \operatorname{Cospan}^{ \mathrm{all}, \mathrm{iso}}(\operatorname{\mathcal{E}})$, where the target is an $\infty $-category (Proposition 8.1.7.5). It follows that the simplicial set $\operatorname{Cospan}^{L',R'}(\operatorname{\mathcal{E}}\times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}})$ is also an $\infty $-category.

Let $\operatorname{ev}_0, \operatorname{ev}_{1}: \operatorname{Fun}( \operatorname{\mathcal{C}}\times \Delta ^1 / \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{E}}$ denote functors given by evaluation at $0,1 \in \Delta ^1$, so that $\operatorname{ev}_0$ and $\operatorname{ev}_1$ determine a functor

By construction we have $\widetilde{L} = \operatorname{ev}^{-1}( L' )$ and $\widetilde{R} = \operatorname{ev}^{-1}( R' )$. Note that $\operatorname{ev}$ is a pullback of the map $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{E}}) = \operatorname{\mathcal{E}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{E}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{E}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$. Moreover, we can identify $V$ with the map

induced by $\operatorname{ev}$. By virtue of Example 8.1.10.13, to show that $V$ is a left fibration, it will suffice to verify the following:

$(0)$

Every element of $\widetilde{L}$ is $\operatorname{ev}$-cocartesian, and every element of $\widetilde{R}$ is $\operatorname{ev}$-cartesian. This follows from Lemma 5.3.7.1.

$(1)$

Fix an object $C \in \operatorname{\mathcal{C}}$ and a morphism $f: X \rightarrow Y$ in the $\infty $-category $\operatorname{\mathcal{E}}_{C}$, which we identify with an object of the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}\times \Delta ^1 / \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$. Let $(u,v): (X',Y') \rightarrow (X,Y)$ be a morphism of $\operatorname{\mathcal{E}}\times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ which belongs to $R'$ (so that $v$ is an isomorphism in $\operatorname{\mathcal{E}}$). Then we can write $(u,v) = \operatorname{ev}(w)$ for some morphism $w: f' \rightarrow f$ in the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}\times \Delta ^1 / \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ (the morphism $w$ then belongs to $\widetilde{R}$ and is therefore automatically $\operatorname{ev}$-cartesian). To prove this, we note that $U(u) = U(v)$ determines an edge $\Delta ^1 \rightarrow \operatorname{\mathcal{C}}$. Replacing $\operatorname{\mathcal{E}}$ by the fiber product $\Delta ^1 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$, we can reduce to the situation where $\operatorname{\mathcal{C}}= \Delta ^1$ is a standard simplex. In this case, we are reduced to the problem of constructing a diagram $\Delta ^1 \times \Delta ^1 \rightarrow \operatorname{\mathcal{E}}$ whose boundary is indicated in the simplex

\[ \xymatrix@R =50pt@C=50pt{ X' \ar@ {-->}[r]^{f'} \ar [d]^{u} & Y' \ar [d]^{v} \\ X \ar [r]^-{f} & Y, } \]

which is possible by virtue of our assumption that $v$ is an isomorphism.

$(2)$

Fix an object $C \in \operatorname{\mathcal{C}}$ and a morphism $f: X \rightarrow Y$ as above, and let $(u,v): (X,Y) \rightarrow (X',Y')$ be a morphism of $\operatorname{\mathcal{E}}\times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ which belongs to $L'$ (so that $u$ is a $U$-cocartesian morphism of $\operatorname{\mathcal{E}}$). Then we can write $(u,v) = \operatorname{ev}(w)$, for some morphism $w: f \rightarrow f'$ in the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}\times \Delta ^1 / \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ (the morphism $w$ then belongs to $\widetilde{L}$ and is therefore automatically $\operatorname{ev}$-cocartesian). This follows from Proposition 5.3.7.2 (or by a direct argument similar to the proof of $(1)$).

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$

Proof. Combine Theorem 11.9.1.12 with Example 11.9.1.7. $\square$