Calculating limits progressively
Let me try to turn my comments into an answer (I think it's also essentially what Vladimir was saying). Suppose you have some diagram $F: K \to \mathcal{C}$. To compute the limit of $F$ is the same as computing the right Kan extension $\epsilon_*F$ along the map $\epsilon: K \to \bullet$. The process you're describing is to compute this Kan extension by factoring the map $\epsilon$ into a bunch of maps $K=K_0 \to K_1 \to K_2 \to \cdots \to \bullet$ and Kan extending one at a time.
That's perfectly allowed. You'd like to keep track of the values of your diagram as you Kan extend. In general, for a functor $p: K \to L$, the value of the right Kan extension $p_*F$ at a point $x \in L$ is given by the limit over the category $K_{x/}$, i.e. the category whose objects are pairs $(k, x \to p(k))$ and whose morphisms are morphisms in $K$ making the appropriate diagram commute.
In general one might ask: when is a limit of a functor $G$ over some diagram $D$ given by just one of the values $G(d)$? A sufficient condition for this to occur is that $d \in D$ be initial.
Putting these two facts together we learn that:
- $p_*F(x)$ is given by a known value of $F$ if $K_{x/}$ has an initial object.
Now you'd like some explicit procedure, I guess, for computing the limit over $K$ in this iterative way where you don't have to change too much at once. Here is one way that works. For ease let's take a skeletal, finite $K$.
- First consider the diagram $K_1$ obtained from $K$ by asking that every endomorphism be the identity. The right Kan extension to this step computes the 'fixed points' of each object under the action of the endomorphisms. If you want, you could do it one object at a time.
- Now begin collapsing parallel arrows one step at a time. This will always be a collapse of the desired type. Indeed, if $a\rightrightarrows b$ is a pair of arrows in $K_i$ and we collapse them to build $K_{i+1}$, then the overcategories $(K_{i+1})_{x/}$ will evidently have initial object $x$ if $x \ne a$. If $x = a$ then we'll be computing an equalizer.
- Now you've got a category $K_N$ where every object has only the identity endomorphism, and there is at most one arrow between any two objects. So you've got a poset! Now you can begin pruning exactly as you did in your example. Arrange the poset by height. Say it has height $n$. If $n$ is zero, then you've got a discrete poset- take the product. Otherwise, if you see two objects of height $(n-1)$ which hit an object of height $n$, form $K_{N+1}$ by collapsing those three objects to a point. This procedure replaces the three objects by the pullback and changes nothing else. Keep doing that until there are no more such objects of height $n$. Either you've decreased the height to $(n-1)$, or there are objects of height $n$ with only one thing of height $(n-1)$ hitting it. Taking each in turn, collapse those pairs to a point. This won't do anything except delete those height $n$ values from your diagram. Now you have something of height $(n-1)$. Repeat until you get down to height 0, then take the product of everything you see.
There are many variations on this theme... you could do things in a different order, or you could embed into a larger diagram which is often convenient, etc. etc.
Of course, there's also the standard formula for a limit as an equalizer of two products, but I imagine you knew that already.
Also- everything I said works for homotopy limits over ordinary categories. If you want to do homotopy limits over an $\infty$-category, you can still do something like this. In fact, said in the language of $\infty$-categories or quasicategories, this whole procedure is maybe more evident: take your quasicategory, which is a simplicial set $K$, and write it as an iterated pushout along cell inclusions (maybe transfinitely many). Then a homotopy colimit over $K$ can be computed by iteratively by using pushouts, or if you come across an empty diagram you'll need an initial object, and then taking filtered colimits along the way. One can take care of limits by working in the opposite category.
This sort of calculus is central to the abstract study of homotopy limits via derivators. See this paper and this one for some examples of "detection lemmas" that decompose limits using Kan extensions in various ways; they all follow from the calculus of homotopy exact squares.