Kerodon

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

Remark 4.5.9.6. In the situation of Proposition 4.5.9.5, postcomposition with the evaluation map $\operatorname{ev}: \operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{B}}} \operatorname{Fun}(\operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{\mathcal{D}}$ induces an isomorphism of simplicial sets

\[ \operatorname{Fun}_{ / \operatorname{\mathcal{B}}}( \operatorname{\mathcal{B}}', \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}}) ) \xrightarrow {\sim } \operatorname{Fun}( \operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{B}}', \operatorname{\mathcal{D}}). \]

The bijectivity of this map on $n$-simplices follows by applying Proposition 4.5.9.5 to the product $\operatorname{\mathcal{B}}' \times \Delta ^ n$.