Corollary 5.3.7.4. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of $\infty $-categories. Then, for every simplicial set $K$, the restriction map
\[ V: \operatorname{Fun}(K^{\triangleleft }, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}( K, \operatorname{\mathcal{E}}) \times _{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \operatorname{Fun}(K^{\triangleleft }, \operatorname{\mathcal{C}}) \]
is also a cocartesian fibration. Moreover, a morphism $f$ in the $\infty $-category $\operatorname{Fun}(K^{\triangleleft }, \operatorname{\mathcal{E}})$ is $V$-cocartesian if and only if evaluation at the cone point of $K^{\triangleleft }$ carries $f$ to a $U$-cocartesian morphism of $\operatorname{\mathcal{E}}$.
Proof.
We have a commutative diagram of $\infty $-categories
\[ \xymatrix@R =50pt{ \operatorname{Fun}(K^{\triangleleft }, \operatorname{\mathcal{E}}) \ar [r]^-{V} \ar [d] & \operatorname{Fun}( K^{\triangleleft }, \operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \operatorname{Fun}(K, \operatorname{\mathcal{E}}) \ar [r] \ar [d] & \operatorname{Fun}(K^{\triangleleft }, \operatorname{\mathcal{C}}) \ar [d] \\ \operatorname{\mathcal{E}}\vec{\times }_{ \operatorname{Fun}(K, \operatorname{\mathcal{E}}) } \operatorname{Fun}(K, \operatorname{\mathcal{E}}) \ar [r]^-{V'} & \operatorname{\mathcal{C}}\vec{\times }_{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \operatorname{Fun}(K, \operatorname{\mathcal{E}}) \ar [r] & \operatorname{\mathcal{C}}\vec{\times }_{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \operatorname{Fun}(K, \operatorname{\mathcal{C}}), } \]
where the right square is a pullback diagram and the outer vertical maps are the equivalences supplied by Example 4.6.4.9. It follows from Proposition 5.3.7.2 that $V'$ is a cocartesian fibration, and that a morphism in the $\infty $-category $\operatorname{\mathcal{E}}\vec{\times }_{ \operatorname{Fun}(K, \operatorname{\mathcal{E}}) } \operatorname{Fun}(K, \operatorname{\mathcal{E}})$ is $V'$-cocartesian if and only if its image in $\operatorname{\mathcal{E}}$ is $V$-cocartesian. Moreover, the morphism $V$ is an isofibration (Proposition 4.4.5.1). By virtue of Theorem 5.1.6.1, it will suffice to show that the middle horizontal map is also an equivalence of $\infty $-categories. This follows from Corollary 4.5.3.33, since the right horizontal maps are pullbacks of the isofibration $U^{K}: \operatorname{Fun}(K, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}(K, \operatorname{\mathcal{C}})$ (Corollary 4.4.5.6.
$\square$