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?