# Kerodon

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

Proposition 5.1.3.4. Let $q_{X}: X \rightarrow S$ and $q_{Y}: Y \rightarrow S$ be morphisms of simplicial sets. If $q_{Y}$ is either a left fibration or a right fibration, then the simplicial set $\operatorname{Fun}_{/S}(X,Y)$ is a Kan complex.

Proof. Without loss of generality, we may assume that $q_{Y}$ is a left fibration. Then postcomposition with $q_{Y}$ induces a left fibration $Q_{Y}: \operatorname{Fun}(X,Y) \rightarrow \operatorname{Fun}(X,S)$ (Corollary 4.2.3.2). By construction, $\operatorname{Fun}_{/S}(X,Y)$ is a fiber of the morphism $Q_{Y}$, and is therefore a Kan complex by virtue of Corollary 4.4.2.2. $\square$