Kerodon

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

Corollary 3.1.3.3. Let $X_{}$ be a Kan complex. Then, for every monomorphism of simplicial sets $i: A_{} \hookrightarrow B_{}$, the restriction map $\operatorname{Fun}( B_{}, X_{} ) \rightarrow \operatorname{Fun}( A_{}, X_{} )$ is a Kan fibration.