# Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$

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.