Kerodon

Proof. As in the proof of Lemma 5.3.6.11, we may assume without loss of generality that $\operatorname{\mathcal{B}}= \Delta ^1$, so that $\operatorname{\mathcal{C}}$ is an $\infty $-category and $\overline{e}$ corresponds to a morphism $T: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{E}}$. Replacing $\operatorname{\mathcal{D}}$ by the fiber product $\operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{E}}} \operatorname{\mathcal{D}}$, we can further reduce to the case where $\operatorname{\mathcal{C}}= \operatorname{\mathcal{E}}$ and $T$ is the identity functor (so that $V: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ is a cartesian fibration of $\infty $-categories). Let $\operatorname{\mathcal{C}}(0)$ and $\operatorname{\mathcal{C}}(1)$ denote the fibers of $\operatorname{\mathcal{C}}$ over the the vertices $0,1 \in \Delta ^1$, so that we can identify $Y$ with a functor $\operatorname{\mathcal{C}}(1) \rightarrow \operatorname{\mathcal{D}}$ such that $V \circ Y$ is the inclusion map $\operatorname{\mathcal{C}}(1) \hookrightarrow \operatorname{\mathcal{C}}$. Applying Proposition 5.2.2.8, we can choose a functor $F: \operatorname{\mathcal{C}}(0) \rightarrow \operatorname{\mathcal{C}}(1)$ and a diagram

which exhibits $F = H|_{ \{ 1\} \times \operatorname{\mathcal{C}}(0) }$ as given by covariant transport along the nondegenerate edge of $\operatorname{\mathcal{B}}= \Delta ^1$. Since $V$ is a cartesian fibration, Proposition 5.2.1.3 guarantees that the lifting problem

admits a solution with the property that, for every object $C$ of the $\infty $-category $\operatorname{\mathcal{C}}(0)$, the restriction $G|_{ \Delta ^1 \times \{ C\} }$ is a $V$-cartesian morphism of $\operatorname{\mathcal{D}}$.

Let $\operatorname{\mathcal{C}}' = (\Delta ^1 \times \operatorname{\mathcal{C}}(0)) {\coprod }_{ (\{ 1\} \times \operatorname{\mathcal{C}}(0)) } \operatorname{\mathcal{C}}(1)$ denote the mapping cylinder of the functor $F$. Amalgamating $H$ with the inclusion map $\operatorname{\mathcal{C}}(1) \hookrightarrow \operatorname{\mathcal{C}}$, we obtain a morphism of simplicial sets $\overline{H}: \operatorname{\mathcal{C}}' \rightarrow \operatorname{\mathcal{C}}$ which is a categorical equivalence by virtue of Corollary 5.2.4.2. Amalgamating $G$ with $Y$, we obtain a diagram $\overline{G}: \operatorname{\mathcal{C}}' \rightarrow \operatorname{\mathcal{D}}$ satisfying $V \circ \overline{G}= \overline{H}$. We have a commutative diagram of simplicial sets

where the horizontal maps are equivalences of $\infty $-categories. Since $V$ is an isofibration, the vertical maps in this diagram are isofibrations (Proposition 4.5.5.14). Applying Corollary 4.5.2.32, we deduce that the upper horizontal map in the diagram (5.32) restricts to an equivalence of the fibers of the vertical maps over the object $Y \in \operatorname{Fun}_{ /\operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}(1), \operatorname{\mathcal{D}})$. It follows that there there exists a functor $E: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ such that $V \circ E = \operatorname{id}_{\operatorname{\mathcal{C}}}$, $E|_{\operatorname{\mathcal{C}}(1)} = Y$, and $E \circ \overline{H}$ is isomorphic to $\overline{G}$ as an object of the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}', \operatorname{\mathcal{D}})$. By construction, we can identify $E$ with an edge $e: X \rightarrow Y$ of $\operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}})$ satisfying $V'(e) = \overline{e}$. To complete the proof, it will suffice to show that $e$ satisfies condition $(\ast )$ of Proposition 5.3.6.6. Let $f: C \rightarrow C'$ be a $U$-cocartesian morphism of $\operatorname{\mathcal{C}}$; we wish to show that $E(f)$ is a $V$-cartesian morphism of $\operatorname{\mathcal{D}}$. Without loss of generality, we may assume that $U(f)$ is the nondegenerate edge of $\operatorname{\mathcal{B}}= \Delta ^1$ (otherwise, $f$ is an isomorphism and there is nothing to prove). By virtue of Remark 5.1.3.8, we can assume without loss of generality that $f: C \rightarrow F(C)$ is the $U$-cocartesian morphism given by the restriction $H|_{ \Delta ^1 \times \{ C\} }$. In this case, $E(f)$ is isomorphic (as an object of the $\infty $-category $\operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{D}})$) to the $V$-cartesian morphism $G|_{ \Delta ^1 \times \{ C\} }$, and is therefore also $V$-cartesian (Corollary 5.1.2.5). $\square$