# Kerodon

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

Proposition 4.1.4.4. Let $q: X \rightarrow S$ be an inner fibration of simplicial sets, and let $i: A \hookrightarrow B$ be an inner anodyne morphism of simplicial sets. Then the restriction map

$\rho : \operatorname{Fun}(B,X) \rightarrow \operatorname{Fun}(A,X) \times _{ \operatorname{Fun}(A,S) } \operatorname{Fun}(B,S)$

is a trivial Kan fibration.

Proof. We wish to show that every lifting problem

$\xymatrix@C =100pt{ A'_{} \ar [d]^{i'} \ar [r] & \operatorname{Fun}( B_{}, X_{} ) \ar [d]^{\rho } \\ B'_{} \ar@ {-->}[ur] \ar [r] & \operatorname{Fun}( B_{}, S_{} ) \times _{ \operatorname{Fun}( A_{}, S_{} )} \operatorname{Fun}( A_{}, X_{} ) }$

admits a solution, provided that $i'$ is a monomorphism of simplicial sets. Equivalently, we must show that every lifting problem

$\xymatrix@C =100pt{ (A_{} \times B'_{} ) \coprod _{ A_{} \times A'_{} } ( B_{} \times A'_{} ) \ar [r] \ar [d] & X_{} \ar [d]^{q} \\ B_{} \times B'_{} \ar [r] \ar@ {-->}[ur] & S_{} }$

admits a solution. This follows from Proposition 4.1.3.1, since the left vertical map is inner anodyne (Lemma 1.4.7.5) and $q$ is an inner fibration. $\square$