= Solution
The categorical <commutation of iterated categorical limits> theorem is the following. For small categories $I,J$ and a two-variable <functor> $F:I\times J\to\mathcal D$, if the two collections of inner limits and their outer limits exist, then there are canonical <isomorphisms>
$$
\boxed{\lim_j\lim_iF(i,j)\cong\lim_{I\times J}F\cong\lim_i\lim_jF(i,j).}
$$
In particular all these limits exist if $\mathcal D$ has all $I$-shaped and all $J$-shaped limits. The <isomorphisms> are natural in $F$ and uniquely characterized by preserving every projection to $F(i,j)$.
Part (iii) proves that each iterated limit represents the <functor> of cones on the product diagram, with the same flattened projections. Two such representations have unique inverse cone-compatible arrows, proving the <isomorphisms>. For a <natural transformation> $F\to F'$, the two composites in any naturality square have the same product-diagram projections, hence agree by limit uniqueness. This proves naturality as well. Completeness of $\mathcal D$ is a convenient sufficient hypothesis, rather than a necessary one for this individual diagram.
Back to article page
