Commutation of limits and colimits: Is there a choice diagram? I was looking at this question about a "soft proof" of the fact that finite limits (shape $I$) commute with filtered colimits (shape $J$) in Set, using only the fact that the diagonal $J \to J^I$ is final.
If we consider the simple case of intersection and unions of sets $A_{i,j}$, we have the formula
$$\bigcap_{i \in I}\bigcup_{j \in J} A_{i,j} = \bigcup_{f : I \to J} \bigcap_{i \in I} A_{i,f(i)}$$
where $f : I \to J$ is a "skolemization" of the existential quantifier on the left hand side (This requires AC for infinite $I$). I am wondering if in the same vein, a limit-of-colimits can be replaced by a colimit-of-limits over a diagram category.

That is, do we have for every diagram $A: I \times J \to \mathbf{Set}$ ($I$ possibly finite) that
$$\mathrm{lim}_{i \in I}\mathrm{colim}_{j \in J}\; A(i,j) \cong \mathrm{colim}_{F \in J^I} \mathrm{lim}_{i \in I}\; A(i,F(i))$$

In this case, using the finality of $I \to J^I$ we'd obtain the desired commutation
$$\mathrm{lim}_{i \in I}\mathrm{colim}_{j \in J}\; A(i,j) \cong \mathrm{colim}_{j \in J} \mathrm{lim}_{i \in I}\; A(i,j)$$
So the formula should hold for $I$ finite $J$ filtered, and I've checked it for $J$ discrete as well if I'm not mistaken. In general, going from the lhs to the rhs requires to build up a skolemizing diagram $F$ not only on objects but on morphisms as well, which seems to involve some complicated choice. Is a formula like the above known, or is my intuition off somewhere?
 A: This isn't true in general. Take $I = BG$ and $J = BH$ to be one-object groupoids, so that $A(i, j)$ becomes a set $A$ with commuting actions of $G$ and $H$. The left hand side is obtained by taking the $H$-orbits of $A$, and then the $G$-fixed points of the result. The right hand side isn't as easy to describe precisely, but it's some quotient of the coproduct over all group homomorphisms $f : G \to H$ of the elements of $A$ fixed by the action of $(g, f(g))$ for every $g \in G$.
Take $G = \mathbb{Z}/2$, $H = \mathbb{Z}$ and let $A = \mathbb{Z}/2$ with action of both $G$ and $H$ given by addition (mod 2). Then $A$ has a single $H$-orbit, which is (obviously) fixed by $G$, so the left hand side has a single element. On the other hand, the only group homomorphism $f : \mathbb{Z}/2 \to \mathbb{Z}$ is the zero map, and there aren't any elements of $A$ fixed by the action of $(g, 0)$ for $g = 1 \in \mathbb{Z}/2$, so the right hand side is empty.
What went wrong in this example? Well, let's try to construct an isomorphism between the two sides anyways. Given an element $x$ on the left, we should try to construct a "corresponding" group homomorphism $f : G \to H$ (not necessarily uniquely determined). The element $x$ is an $H$-orbit of $A$ which is fixed by $G$. Let's pick an element $a \in A$ of this orbit. Then for each $g \in G$, since $ga$ generates the same orbit as $a$, there must be some $h \in H$ with $(g, h)a = a$. We would like to send $x$ to the rule $f$ which maps $g$ to such an $h$. However, $h$ is only well-defined as an element of some quotient of $H$, namely the quotient by the subgroup which fixes $a$ (or $ga$, since the actions commute). So we obtain a group homomorphism from $G$ to a quotient of $H$, but it might not lift to $H$ itself.
One thing I'm not sure about is what happens in the $\infty$-category of spaces, which generally has better exactness properties since there is no set-truncation in the construction of colimits. If the isomorphism holds there, then one could recover the version for sets when $J$ is filtered, since filtered colimits of sets are also homotopy colimits.
