Proposition 3.4.0.7. Let $f_0: X_0 \rightarrow X$ and $f_1: X_1 \rightarrow X$ be morphisms of simplicial sets. Assume that $X$ is a Kan complex and that either $f_0$ or $f_1$ is a Kan fibration. Then the inclusion map $X_0 \times _{X} X_1 \rightarrow X_{0} \times _{X}^{\mathrm{h}} X_1$ is a weak homotopy equivalence.
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proof. Without loss of generality we may assume that $f_0$ is a Kan fibration. Since $X$ is a Kan complex, the evaluation map $\operatorname{ev}_0: \operatorname{Fun}(\Delta ^1, X) \rightarrow \operatorname{Fun}(\{ 1\} , X)$ is a trivial Kan fibration (Corollary 3.1.3.6), and therefore induces a trivial Kan fibration $q: \operatorname{Fun}(\Delta ^1,X) \times _{ \operatorname{Fun}(\{ 1\} , X) } X_1 \rightarrow X_1$. The diagonal map $\delta : X \hookrightarrow \operatorname{Fun}(\Delta ^1,X)$ determines a map $s: X_1 \rightarrow \operatorname{Fun}(\Delta ^1,X) \times _{ \operatorname{Fun}(\{ 1\} , X) } X_1$ which is a section of $q$, and therefore also a weak homotopy equivalence. The desired result now follows by applying Proposition 3.4.0.2 to the diagram
\[ \xymatrix@R =50pt@C=50pt{ X_0 \ar@ {=}[d] \ar [r]^-{f_0} & X \ar@ {=}[d] & X_1 \ar [l]_{f_1} \ar [d]^{s} \\ X_0 \ar [r]^-{f_0} & X & \operatorname{Fun}( \Delta ^1, X) \times _{ \operatorname{Fun}(\{ 1\} , X) } X_1. \ar [l] } \]
$\square$