Often when computing in category theory, one has to show that some square is cartesian. Depending on the number of maps involved, and their arrangement, it's somewhat difficult to write down exactly all of the relationships between the various squares.

Take for instance the following problem (please don't answer it, I've already proven it):

We have a commutative diagram

$$\begin{matrix}C_3 &\to& C_2 &\to& C_1\\ \downarrow&&\downarrow&&\downarrow\\ D_3&\to &D_2&\to& D_1 \end{matrix}$$

Label the right vertical map $p$, and assume we further have a commutative diagram

$$\begin{matrix}\ast &\to& C_1\\ \downarrow&&\downarrow\\ D_3&\to& D_1 \end{matrix}$$

Where map on the top of the square is called $x$ (it classifies a point $x$, and the left vertical map is called $\sigma$. The bottom map and right map are the same maps from the first diagram $D_3\to D_1$ is simply the composite of the two bottom maps in the first diagram.

We would like to show that the canonical map between fibers $$C_3\times_{D_3\times_{D_1} C_1} \{\sigma,x\}\to C_2\times_{C_1} \{x\}\times_{D_2\times_{D_1} \{px\}}\{e\}$$ is a pullback of the canonical map $C_3\to C_2\times_{D_2} D_3$ (if you really care to know, this is to show that the first map is a trivial fibration, since we knew at the time that the second map was a trivial fibration).

Note: The vertex $\{e\}$ is the image of $\sigma$ in $D_2$.

The diagram I drew to realize this was a sheet of four cartesian squares with a cartesian cube attached at the top left square. This is before even taking fibers.

Another example: If anyone's following Ravi Vakil's notes for his schemes course, there is a similar, albeit substantially less complicated problem to prove that the "magic square" is cartesian. I did a similar computation, which ended again with the surprising cartesianness ultimately arising from a cartesian cube attached to a cartesian sheet.

Then the question: Is there a more efficient way to verify claims like this (i.e. without drawing out "every single possible pullback"?

subsetof it (e.g. "this bit is a pullback of this bit so there's a map from here to here that makes this triangle commute") to draw in another arrow, and I wanted to verify that the new diagram was a commutative diagram! The first time I ran into this issue I had to think hard about what the correct definition... – Kevin Buzzard Sep 18 '10 at 9:55