$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proposition 3.4.0.2. Suppose we are given a commutative diagram of simplicial sets
\[ \xymatrix@R =50pt@C=50pt{ X_0 \ar [d] \ar [r]^-{f} & X \ar [d] & X_1 \ar [l] \ar [d] \\ Y_0 \ar [r]^-{f'} & Y & Y_1, \ar [l] } \]
where the vertical maps are weak homotopy equivalences. If $f$ and $f'$ are Kan fibrations, then the induced map $X_0 \times _{X} X_1 \rightarrow Y_0 \times _{Y} Y_1$ is a weak homotopy equivalence.
Proof.
We have a commutative diagram
\[ \xymatrix@R =50pt@C=50pt{ X_0 \times _{X} X_1 \ar [r] \ar [d] & Y_0 \times _{Y} Y_1 \ar [d] \\ X_1 \ar [r] & Y_1, } \]
where the vertical maps are Kan fibrations (since they are pullbacks of $f$ and $f'$, respectively). By virtue of Proposition 3.3.7.1, it will suffice to show that for each vertex $x \in X_1$ having image $y \in Y_1$, the induced map of fibers
\[ (X_0 \times _{X} X_1)_{x} \simeq X_0 \times _{X} \{ x\} \rightarrow Y_0 \times _{Y} \{ y\} = (Y_0 \times _{Y} Y_1)_{y} \]
is a homotopy equivalence of Kan complexes. This follows by applying Proposition 3.3.7.1 to the diagram
\[ \xymatrix@R =50pt@C=50pt{ X_0 \ar [d]^{f} \ar [r] & Y_0 \ar [d]^{f'} \\ X \ar [r] & Y. } \]
$\square$