Kerodon

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

Corollary 4.8.4.8. Let $n \geq -1$ be an integer and let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}'$ be a functor of $\infty $-categories which exhibits $\operatorname{\mathcal{C}}'$ as a homotopy $n$-category of $\operatorname{\mathcal{C}}$ (Definition 4.8.4.1). Then $F$ exhibits $\operatorname{\mathcal{C}}'$ as a local $(n-1)$-truncation of $\operatorname{\mathcal{C}}$ (Definition 4.8.2.9).

Proof. Since $\operatorname{\mathcal{C}}'$ is an $(n,1)$-category, it is locally $(n-1)$-truncated (Example 4.8.2.2). It will therefore suffice to show that, for every locally $(n-1)$-truncated $\infty $-category $\operatorname{\mathcal{D}}$, precomposition with $F$ induces an equivalence of $\infty $-categories $\theta : \operatorname{Fun}( \operatorname{\mathcal{C}}', \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ (Proposition 4.8.2.18). By virtue of Corollary 4.8.3.3, we may assume that $\operatorname{\mathcal{D}}$ is an $(n,1)$-category. In this case, Proposition 4.8.4.7 guarantees that $\theta $ is an isomorphism of simplicial sets. $\square$