Kerodon

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

Proof. By virtue of Theorem 2.4.5.1, it suffices to show that the simplicial category $\operatorname{Kan}$ is locally Kan: that is, for every pair of Kan complexes $X$ and $Y$, the simplicial set $\operatorname{Fun}(X,Y)$ is also a Kan complex. This is a special case of Corollary 3.1.3.4. $\square$