Commutation of iterated categorical limits (source code)

= Commutation of iterated categorical limits
{title2=$\lim_j\lim_kD(j,k)\cong\lim_k\lim_jD(j,k)$}

For small $J,K$ and a <functor> $D:J\times K\to\mathcal C$ into a <complete category>, the two iterated <categorical limits> are canonically isomorphic. They have the same projections to every $D(j,k)$ and the same <universal property>. The result follows also from preservation of <categorical limits> by the <limit functor>.