Kerodon

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

Theorem 3.1.3.5. Let $i: A_{} \hookrightarrow B_{}$ be an anodyne morphism of simplicial sets and let $f: X_{} \rightarrow S_{}$ be a Kan fibration. Then the induced map

$\operatorname{Fun}( B_{}, X_{} ) \rightarrow \operatorname{Fun}( B_{}, S_{} ) \times _{ \operatorname{Fun}( A_{}, S_{} )} \operatorname{Fun}( A_{}, X_{} )$

is a trivial Kan fibration.

Proof. We proceed as in the proof of Theorem 3.1.3.1. Let $i': A'_{} \hookrightarrow B'_{}$ be a monomorphism of simplicial sets; we must show that every lifting problem

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

admits a solution. 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]^{f} \\ B_{} \times B'_{} \ar [r] \ar@ {-->}[ur] & S_{} }$

admits a solution. This follows from Remark 3.1.2.7, since the left vertical map is anodyne (Proposition 3.1.2.8) and the right vertical map is a Kan fibration. $\square$