# Kerodon

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

Remark 4.5.9.3. In the situation of Proposition 4.5.9.2, composition with the evaluation map $\operatorname{ev}: \operatorname{\mathcal{D}}\times _{\operatorname{\mathcal{C}}} \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{E}}$ induces an isomorphism of simplicial sets

$\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}', \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}}) ) \xrightarrow {\sim } \operatorname{Fun}_{ / \operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}}).$

The bijectivity of this map on $n$-simplices follows by applying Proposition 4.5.9.2 after replacing $\operatorname{\mathcal{C}}'$ by the product $\Delta ^ n \times \operatorname{\mathcal{C}}'$.