Kerodon

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

Corollary 3.5.7.30. Let $n$ be an integer and let $\mathrm{h} \mathit{\operatorname{Kan}}^{\leq n}$ denote the full subcategory of the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$ spanned by the $n$-truncated Kan complexes. Then the inclusion map $\mathrm{h} \mathit{\operatorname{Kan}}^{\leq n} \hookrightarrow \mathrm{h} \mathit{\operatorname{Kan}}$ admits a left adjoint, given by the construction $X \mapsto \operatorname{cosk}_{n+1}(X)$.