Kerodon

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

Corollary 3.1.7.7. Let $\operatorname{\mathcal{C}}$ be a category, let $\operatorname{\mathcal{E}}\subseteq \operatorname{Fun}( \operatorname{Kan}, \operatorname{\mathcal{C}})$ be the full subcategory spanned by those functors $F: \operatorname{Kan}\rightarrow \operatorname{\mathcal{C}}$ which carry homotopy equivalences of Kan complexes to isomorphisms in the category $\operatorname{\mathcal{C}}$. Then precomposition with the quotient map $\operatorname{Kan}\rightarrow \mathrm{h} \mathit{\operatorname{Kan}}$ induces an isomorphism of categories $\operatorname{Fun}( \mathrm{h} \mathit{\operatorname{Kan}}, \operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{E}}$.