Kerodon

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)$).