Kerodon

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

Remark 3.4.2.3. Let $f_0: A \rightarrow A_0$ and $f_1: A \rightarrow A_1$ be morphisms of simplicial sets, and let $X$ be a Kan complex. Then the simplicial set $\operatorname{Fun}(A, X)$ is a Kan complex (Corollary 3.1.3.4), and we have a canonical isomorphism

\[ \operatorname{Fun}( A_{0} {\coprod }_{A}^{\mathrm{h}} A_{1}, X) \simeq \operatorname{Fun}( A_0, X) \times _{\operatorname{Fun}(A,X)}^{\mathrm{h}} \operatorname{Fun}(A_1, X), \]

where the right hand side is the homotopy fiber product of Construction 3.4.0.3.