# Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$

Proposition 5.1.3.5. Let $q_{X}: X \rightarrow S$ and $q_{Y}: Y \rightarrow S$ be morphisms of simplicial sets, and let $X' \subseteq X$ be a simplicial subset. If $q_{Y}$ is either a left fibration or a right fibration, then the restriction map $\theta : \operatorname{Fun}_{/S}(X, Y) \rightarrow \operatorname{Fun}_{/S}(X', Y)$ is a Kan fibration.

Proof. Without loss of generality, we may assume that $q_{Y}$ is a left fibration. By construction, we have a pullback diagram of simplicial sets

$\xymatrix@R =50pt@C=50pt{ \operatorname{Fun}_{/S}(X,Y) \ar [r] \ar [d]^{\theta } & \operatorname{Fun}(X,Y) \ar [d]^{\theta '} \\ \operatorname{Fun}_{/S}(X', Y) \ar [r] & \operatorname{Fun}(X',Y) \times _{ \operatorname{Fun}(X',S)} \operatorname{Fun}(X,S). }$

Proposition 4.2.3.1 guarantees $\theta '$ is a left fibration, so that $\theta$ is also a left fibration (Remark 4.2.1.8). Since $\operatorname{Fun}_{/S}(X',Y)$ is a Kan complex (Proposition 5.1.3.4), it follows that $\theta$ is also a Kan fibration (Lemma 5.1.2.4). $\square$