How to formally -- and cleanly -- express relationships of limits of diagrams?

Question

Requesting: a good reference for formal manipulation of limits of diagrams, with respect to maps of index diagrams.

As an example, consider the following result, for some "nice enough" category C (say, Top), there is a natural isomorphism $$(A \times_B C) \times_C D \cong A \times_B D.$$ This is a nice, intuitively true result that if we stick two pullback squares next to each other, we get another pullback square. I can easily convince myself of this on paper, chasing around the requisite number of arrows -- and it's a simple enough result that no wizardry is required; all maps could be named and the necessary commutativity relations and existence/uniqueness conditions can be checked.

However, it's a bit unsatisfactory. There's a blow-up of notation required to prove a relatively simple result. What happens when the diagrams get more complicated? It becomes less clear how proving basic results about limits can be written up with an acceptable amount of rigor, while remaining concise.

A general question of this type: let $C$ be a complete category, and let $D,E$ be small categories. A functor $f : D \to E$ induces a functor $f^* : C^E \to C^D$. For which $f$ is it the case that $\lim_E = \lim_D \circ f^*$ as functors $C^E \to C$?

It is at least intuitively clear that if $f(D)$ sufficiently "sits above" $E$, then this will hold. I am interested in formalizing this intuition.

I'm sure this question must have a standard answer in category theory, but a sufficient reference escapes me at the moment.

Answer 1

As was mentioned in the comments, such general isomorphisms can be reduced by Yoneda to the case of sets, and in your example $((a,c),d) \mapsto (a,d)$ is an isomorphism, simply because $c$ is already determined by $d$. As for me, I always manipulate arrows without caring about single-use names and use Yoneda. This worked very good in the past years. For example, for every test object $T \in C$, we have canonical bijections

$\{T \to (A \times_B C) \times_C D\} = \{T \to A \times_B C \to C = T \to D \to C\}$ $= \{T \to A \to B = T \to C \to B, T \to C = T \to D \to C\}$ $=\{T \to A \to B = T \to D \to C \to B\} = \{T \to A \times_B D\}$

You may argue that it's not clear at all what is given etc., but there is only one plausible interpretation: Everything not given before belongs to the data of the morphism sets. Every equation is a condition on this data. It's even nicer to draw everything in commutative diagrams (I don't know how to draw them here). This method also works when you want to simplify a universal object without knowing the result. You just reduce the diagrams as above. Every step is almost forced. Of course, this is just another way of writing down the proof mentioned first.

Regarding your second question: Your intuition is absolutely correct. A sufficient and useful condition is that $f$ is a final functor. You can read about them in Mac Lane, Categories for the working mathematician, IX.3.