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"?



Efficiently computing with pullbacks and pushouts
Try doing it in sets; then you can usually write it out "syntactically". It looks like you've got a map
$$ \{c\_3\in C\_3|p(c\_3)=\sigma, fg(c\_3)=x\} \to \{c\_2 \in C\_2| f(c\_2)=x \}$$
sending $c\_3\mapsto g(c\_3)$
and you want to know it's the pullback of the map 
$$ \{c\_3\in C\_3\} \to \{(c\_2,d\_3)| p(c\_2)=g(d\_3)\}$$
sending $c\_3\mapsto (g(c\_3),p(c\_3))$. 
I'm writing "$p$" for all vertical maps, "$g$" for $C\_3\to C\_2$ and $D\_3\to D\_2$, and "$f$" for $C\_2\to C\_1$ and $D\_2\to D\_1$. 


Having done this, your claim looks false: it looks like the pullback set is just $\{c\_3\in C\_3|gf(c\_3)=x\}$. But quite possibly I've misinterpreted your diagrams.


The point of this exercise is that, if the set theoretic argument holds, then you can prove the version in the category $C$ using the Yoneda lemma; apply $\mathrm{Hom}\_{\mathcal{C}}(T,{-})$ to everything, for arbitrary objects $T$, and observe you get a pullback of sets, therefore you must have a pullback in $\mathcal{C}$. 


