be a pushout square in \(T\). Let \(Q_0 \leftarrow P_0 \to R_0\) be a span over \(B \leftarrow A \to C\), and write
\[S := Q_0 \sqcup_{P_0} R_0.\]
Then the colimit span \(Q_{\infty} \leftarrow P_{\infty} \to R_{\infty}\) from Construction 5.26 has pushout \(S\), and the canonical maps
\[Q_{\infty} \to S \times_D B, \qquad
P_{\infty} \to S \times_D A, \qquad
R_{\infty} \to S \times_D C\]
are isomorphisms.
Proof
By Construction 5.24, each step in the zigzag construction preserves the pushout of the span. Since colimits commute with colimits, the pushout of \(Q_{\infty} \leftarrow P_{\infty} \to R_{\infty}\) is again \(S\).For odd \(n\), the map \(P_n \to Q_n\) is cartesian over \(A \to B\) by construction. Since the odd natural numbers are cofinal in \(\N\), and since sequential colimits in a topos are universal, it follows that \(P_{\infty} \to Q_{\infty}\) is cartesian over \(A \to B\). Similarly, using the even stages, \(P_{\infty} \to R_{\infty}\) is cartesian over \(A \to C\).Now compare the pushout square \(Q_{\infty} \sqcup_{P_{\infty}} R_{\infty} \simeq S\) with the original pushout square \(B \sqcup_A C \simeq D\): The left and back faces of the cube are cartesian by the previous paragraph, while the top and bottom faces are pushouts. Descent for pushouts therefore implies that the front and right faces are cartesian. This gives \(Q_{\infty} \iso S \times_D B\) and \(R_{\infty} \iso S \times_D C\), and then also \(P_{\infty} \iso S \times_D A\).
