Homotopy pullbacks of spaces become pullbacks of animae

Proof. Consider continuous maps \(f\colon X \to Z\) and \(g\colon Y \to Z\), and consider the pullback square

defining \(X \times _Z^{h} Y\). The path fibration \(p\) is a Serre fibration by Lemma 2.3.17, hence this square is sent to a pullback square in \(\An \) by Proposition 2.3.19. The canonical inclusion \(i\colon X \hookrightarrow P(f)\) is a homotopy equivalence, giving an equivalence \(\Pi _{\infty }(P(f)) \simeq \Pi _{\infty }(X)\). This finishes the proof. □