Corollary 7.6.4.21. Let $f_0, f_1: Y \rightarrow X$ be morphisms of Kan complexes. Then the homotopy equalizer $\operatorname{hEq}(f_0, f_1)$ is a Kan complex, which is an equalizer of $f_0$ and $f_1$ in the $\infty $-category $\operatorname{\mathcal{S}}$.
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$