Kerodon

Proof. Let $\pi : \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{C}}$ denote the projection map and let $f: \operatorname{\mathcal{C}}' \rightarrow \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}})$ be a morphism satisfying $\pi \circ f = W$, corresponding to a morphism of simplicial sets $F: \operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ for which $V \circ F$ is given by projection to the second factor. Note that we can regard $F$ as a vertex of the simplicial subset $\operatorname{Fun}^{\operatorname{CCart}}_{/\operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}})$ if and only if it satisfies the following condition:

$(a)$

For every edge $(e',e)$ of the fiber product $\operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}$ for which $e'$ is a $W$-cocartesian edge of $\operatorname{\mathcal{C}}'$, the image $F(e',e)$ is a $V$-cocartesian edge of $\operatorname{\mathcal{E}}$.

We wish to show that $(a)$ is equivalent to the following pair of conditions:

$(b)$

The morphism $f$ factors through the full simplicial subset $\operatorname{Res}^{\operatorname{CCart}}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}}) \subseteq \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}})$. In other words, for every edge $(e',e)$ of the fiber product $\operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}$ for which $e'$ is a degenerate edge of $\operatorname{\mathcal{C}}'$, the image $F(e',e)$ is a $V$-cocartesian edge of $\operatorname{\mathcal{E}}$.

$(c)$

For every $W$-cocartesian edge $e'$ of $\operatorname{\mathcal{C}}'$, the image $f(e')$ is a $\pi |_{ \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}}) }$-cocartesian edge of $\operatorname{Res}^{\operatorname{CCart}}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}})$. By virtue of Propositions 5.3.7.9 and 5.3.6.6, this is equivalent to the assertion that for every edge $(e',e)$ of the fiber product $\operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}$ where $e'$ is $W$-cocartesian and $e$ is $U$-cartesian, the image $F(e',e)$ is a $V$-cocartesian edge of $\operatorname{\mathcal{E}}$.

The implications $(a) \Rightarrow (b)$ and $(a) \Rightarrow (c)$ are clear. For the converse, suppose that $(b)$ and $(c)$ are satisfied; we wish to prove $(a)$. Let $(e',e): (X',X) \rightarrow (Z',Z)$ be an edge of the fiber product $\operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}$, where $e': X' \rightarrow Z'$ is $W$-cocartesian. Let $\overline{e} = U(e) = W(e')$ denote the corresponding edge of $\operatorname{\mathcal{C}}$. Since $U$ is a cartesian fibration, there exists a $U$-cartesian morphism $f: Y \rightarrow Z$ satisfying $U(f) = \overline{e}$. Let $\overline{\sigma }$ denote the left-degenerate $2$-simplex $s^{1}_0(\overline{e})$. Since $f$ is $U$-cartesian, we can lift $\overline{\sigma }$ to a $2$-simplex of $\operatorname{\mathcal{D}}$ as indicated in the diagram

Writing $\sigma '$ for the left-degenerate $2$-simplex $s^{1}_0(e')$ of $\operatorname{\mathcal{C}}'$, we obtain a $2$-simplex $\tau = F( \sigma ', \sigma )$ of $\operatorname{\mathcal{E}}$. It follows from assumption $(b)$ that the restriction $\tau |_{ \operatorname{N}_{\bullet }( \{ 0 < 1\} ) }$ is a $V$-cocartesian edge of $\operatorname{\mathcal{E}}$, and from assumption $(c)$ that the restriction $\tau |_{ \operatorname{N}_{\bullet }( \{ 1 < 2 \} ) }$ is a $V$-cocartesian edge of $\operatorname{\mathcal{E}}$. Applying Proposition 5.1.4.12, we conclude that $F(e',e) = \tau |_{ \operatorname{N}_{\bullet }( \{ 0 < 2 \} ) }$ is also a $V$-cocartesian edge of $\operatorname{\mathcal{E}}$. $\square$