Commutativity of categorical limits It is known that,  if the limits $\lim _{i\in\mathsf I}\lim_{j\in\mathsf J}G(i,j)$ and $\lim _{j\in\mathsf J}\lim_{i\in\mathsf I}G(i,j)$ associated to a diagram $G:\sf I\times J\to C$ exist in $\sf C$, they are isomorphic; it should follow from the limit functor $\lim:\sf C^J\to C$ preserving limits (it is a right adjoint).

Let $F:\sf I\to C^J$ be a diagram in $\sf C^J$. Denoting with $\circ $ the composition of functors, ($1$) one can take the limit in $\sf C$ of the diagram $\lim \circ \  F:\sf I\to C$; such limit must coincide with ($2$) the image under $\lim$ of the limit of $F$ in $\sf C^J$, because $\lim$ preserves limits. Moreover, calling $\bar F:\sf I\times J\to C$ the exponential transpose of $F$, ($1$) gives $\lim _{i\in\mathsf I}\lim_{j\in\mathsf J}\bar F(i,j)$; since the limit in $\sf C^J$ is computed objectwise, calling $F^*:\sf J\to C^I$ the other transpose of $\bar F$, ($2$) leads to the limit in $\sf C$ of $\lim  \circ \ F^*$, that is $\lim _{j\in\mathsf J}\lim_{i\in\mathsf I}\bar F(i,j)$.

If these arguments make sense, my question is:  can one, with similar arguments, without computations, prove that the limits above  are both isomorphic to the limit of $\sf I\times J\to C$? I don't see it, but probably there is one using exponentials. Thanks for any suggestion.
Edit. In this diagram of categories, let the non-labeled functors be constant, i.e. they send an object of the domain to the corresponding constant diagram. The labeled functors (whose underlying object maps are components of the natural iso $\mathrm {Fun}(-,C^J)\cong \mathrm{Fun} (-\times J,C)$ and of its analogous with $I$) are isos.
$\require{AMScd}$
$$\begin{CD}
C@>>> C^I @>>> (C^I)^J\\
@VVV @. @V\sim VV \\
C^J@>>> (C^J)^I @>\sim >> C^{I\times J}
\end{CD}$$ Both paths from $C$ to $C^{I\times J}$ give the constant functor. Taking the adjoint of every functor (so the inverse of the isos) yields: $$\begin{CD}
C@<<< C^I @<<< (C^I)^J\\
@AAA @. @A\sim AA \\
C^J@<<< (C^J)^I @<\sim << C^{I\times J}
\end{CD}$$ So by the properties of the composition of adjoints, the two paths from $C^{I\times J}$ to $C$ are both adjoint to the constant $C\to C^{I\times J}$.
 A: $\require{AMScd}$My favourite argument to prove this statement with a sleight of hand is to reduce the commutativity of limit functors to the commutativity of their left adjoints, the constant functors: if $\Delta_J \dashv \lim_J$ and $\Delta_J : C \to C^J$ is the constant functor, then the diagram
$$ \begin{CD}
C^I @<\Delta_I<< C @>\Delta_J >> C^J \\
@V\Delta_J VV@VVV@VV\Delta_I V\\
(C^I)^J @= C^{I\times J} @= (C^J)^I
\end{CD}$$
"commutes", if the lower horizontal maps are the identifications $C^{I\times J}\cong (C^I)^J\cong (C^J)^I$. It takes a while to dot all the i's (the left and right vertical functors are not the same diagonal as the horizontal one because the "base" of the constant changes...)  but it's just notational burden, and proving the commutativity is straightforward.
By uniqueness of adjoints, or rather taking the adjoint of each arrow in the square, you get commutativity of limits.
A: One approach is to combine the following facts about right Kan extensions.

*

*$\lim_i G(i,j)$ constitute the pointwise right Kan extension of $G\colon I\times J\to C$ along $F_1\colon I\times J\to J$

*that right Kan extensions along $F_2\colon J\to 1$, where $1$ is the category consisting of a single object and its morphism, are always limits.

*that a right Kan extension along $F_2$ of a right Kan extension along $F_1$, e.g. $\lim_i\lim_j G(i,j)$ is a right Kan extension along $F_2F_1$, e.g. $\lim_{i,j}G(i,j)$.


Explicitly, a right extension of a functor $G\colon I\to C$ along a functor $F\colon I\to J$ consists of a functor $H\colon J\to C$ and a natural transformation $\epsilon\colon HF\Rightarrow G$ that is sometimes called the counit of the right extension. A morphism from a right extension with counit $\epsilon_1\colon H_1F\Rightarrow G$ to a right extension with counit $\epsilon_2\colon H_2F\Rightarrow G$ is a natural transformation $\phi\colon H_1\Rightarrow H_2$ so that $\epsilon_1=\epsilon_2\circ \phi F\colon H_1F\Rightarrow H_2F\Rightarrow GF$.
In the case where $J$ is the category consisting of one object and its identity morphism, a right extension is the same thing as a cone over the diagram given by $G\colon I\to C$, and a morphism of right extension is the same thing as a morphism of cones.
In general, a right Kan extension of $G\colon I\to C$ along $F\colon I\to J$ is a terminal object in the category of such right extensions. In particular, when $J$ is the category consisting of one object and its identity morphism, it is the limiting cone of the diagram represented by $G\colon I\to C$. This shows 2, while 3 is a straightforward exercise.
Seeing 1 is less straightforward even if we assume the non-obvious (weighted) limit formula for pointwise right Kan extensions. The argument goes as follows.
For each object $j$ of $J$ let $(j\downarrow F)$ be the the category whose objects are morphisms $j\to Fi$ and whose morphisms from an object $j\to Fi_1$ to an object $j\to Fi_2$ are morphisms $i_1\to i_2$ in $I$ for which $j\to Fi_2$ factors as $J\to Fi_1\to Fi_2$. Evidently we have a functor $\Pi_{j,F}\colon(j\downarrow F)\to I$ sending $j\to F_i$ to $i$ and a morphism $i_1\to i_2$ to itself.
This functor has a special feature that it is a discrete fibration, which means that it is the result of the Grothendieck construction applied to a functor $I\to\textbf{Set}$; in this case the one sending $i$ to the set of morphisms $j\to Fi$, and $i_1\to i_2$ to the post-composition action sending $j\to Fi_1$ to $j\to Fi_2$.
A cone over a diagram $G\colon I\to C$ weighted by that functor is then simply a cone over $G\Pi_{j,F}\colon(j\downarrow F)\to I\to C$. The weighted limit of $G$ for that weight is then a limiting cone over $G\Pi_{j,F}\colon(j\downarrow F)\to I\to C$.
The pointwise formula for right Kan extensions then says that if the above-described weighted limits exist for each object $j$, then their vertices assemble into a right Kan extension of $G$ along $F$ (and conversely if the right Kan extension is preserved by representable functors).
Now for the projection functor $F\colon I\times J\to J$, we have that $(j\downarrow F)$ has for its objects the pairs $((i,j'),j\to j')$ and for its morphisms pairs $i_1\to i_2$, $j'_1\to j'_2$. In particular, we have a functor $K\colon I\to(j\downarrow F)$ given by $i\mapsto((i,j),\mathrm{id}_j\colon j\to j)$ and $i_1\to i_2\mapsto (i_1\to i_2,\mathrm{id}_j\colon j\to j)$. This functor turns out to be initial: any object of $(j\downarrow F)$ has a morphism with domain in its image.
Consequently, any limit of $G$ weighted by $\pi_{j,F}$ is the same as the limit of $G\pi_{j,F}K$. But $\pi_{j,F}K$ is simply functor $I\to I\times J$ sending $i\mapsto(i,j)$, whence we see that if all the limits $\lim_i G(i,j)$ exist, then they assemble into a right Kan extension of $G$ along $I\times J\to J$.
