Kerodon

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

Corollary 8.1.1.13. Let $\operatorname{\mathcal{C}}$ be a Kan complex. Then the projection map $(\lambda _{-}, \lambda _{+} ): \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}} \times \operatorname{\mathcal{C}}$ is a Kan fibration. In particular, $\operatorname{Tw}(\operatorname{\mathcal{C}})$ is a Kan complex.