Kerodon

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

Corollary 1.5.5.6. Let $p: X \rightarrow Y$ be a trivial Kan fibration of simplicial sets and let $i: A \rightarrow B$ be a monomorphism of simplicial sets. Then the canonical map

\[ \theta : \operatorname{Fun}( B, X ) \rightarrow \operatorname{Fun}( B, Y) \times _{ \operatorname{Fun}( A, Y ) } \operatorname{Fun}( A, X ) \]

is also a trivial Kan fibration.

Proof. Fix an integer $n \geq 0$; we wish to show that every lifting problem

\[ \xymatrix@C =70pt@R=70pt{ \operatorname{\partial \Delta }^ n \ar [r] \ar [d] & \operatorname{Fun}( B, X ) \ar [d]^{\theta } \\ \Delta ^ n \ar@ {-->}[ur] \ar [r] & \operatorname{Fun}( B, Y) \times _{ \operatorname{Fun}( A, Y ) } \operatorname{Fun}( A, X ) } \]

admits a solution. Unwinding the definitions, we see that this is equivalent to solving an associated lifting problem

\[ \xymatrix@C =70pt@R=70pt{ (\operatorname{\partial \Delta }^ n \times B) \underset {\operatorname{\partial \Delta }^ n \times A}{ \coprod } ( \Delta ^ n \times A ) \ar [r] \ar [d]^{i} & X \ar [d]^{p} \\ \Delta ^ n \times B \ar@ {-->}[ur] \ar [r] & Y. } \]

This is possible by virtue of Proposition 1.5.5.4, since $p$ is a trivial Kan fibration and $i$ is a monomorphism. $\square$