Remark 5.3.1.19. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ and $U': \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}$ be cocartesian fibrations of simplicial sets, and let $K$ be an arbitrary simplicial set. Then:
The projection map $\operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \operatorname{Fun}(K, \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{C}}$ is also a cocartesian fibration.
The canonical isomorphism
\[ \operatorname{Fun}(K, \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}}) ) \simeq \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \operatorname{Fun}(K, \operatorname{\mathcal{E}}) ) \]restricts to an isomorphism of full subcategories
\[ \operatorname{Fun}(K, \operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}}) ) \simeq \operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \operatorname{Fun}(K, \operatorname{\mathcal{E}}) ). \]
Both assertions follow immediately from Theorem 5.2.1.1.