Proposition 3.4.2.5. A commutative diagram of simplicial sets
\[ \xymatrix@R =50pt@C=50pt{ A \ar [r] \ar [d] & A_0 \ar [d] \\ A_1 \ar [r] & A_{01} } \]
is a homotopy pushout square if and only if the induced map
\[ \theta : A_0 { \coprod }_{A}^{\mathrm{h}} A_{1} \twoheadrightarrow A_{0} {\coprod }_{A} A_{1} \rightarrow A_{01} \]
is a weak homotopy equivalence of simplicial sets.
Proof.
Let $X$ be a Kan complex, so that $\operatorname{Fun}(A,X)$ is also a Kan complex (Corollary 3.1.3.4). Applying Corollary 3.4.1.6, we see that the diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Fun}(A_{01}, X) \ar [r] \ar [d] & \operatorname{Fun}(A_0,X) \ar [d] \\ \operatorname{Fun}(A_1,X) \ar [r] & \operatorname{Fun}(A,X) } \]
is a homotopy pullback square if and only if the composite map
\[ \rho _{X}: \operatorname{Fun}( A_{01}, X) \rightarrow \operatorname{Fun}( A_0, X) \times _{ \operatorname{Fun}( A,X) } \operatorname{Fun}( A_1, X) \hookrightarrow \operatorname{Fun}( A_{0} ,X) \times ^{\mathrm{h}}_{\operatorname{Fun}(A,X)} \operatorname{Fun}(A_1,X) \]
is a homotopy equivalence. Using the isomorphism of Remark 3.4.2.3, we can identify $\rho _{X}$ with the morphism $\operatorname{Fun}( A_{01}, X) \rightarrow \operatorname{Fun}( A_{0} {\coprod }_{A}^{\mathrm{h}} A_1, X)$ given by precomposition with $\theta $. Proposition 3.4.2.5 now follows by allowing the Kan complex $X$ to vary.
$\square$