Initial functor (source code)

= Initial functor
{wiki}

A functor $F:\mathcal I\to\mathcal J$ is initial when every comma category $(F\downarrow j)$ is nonempty and connected. Restriction along an initial functor preserves limits:
$$
\lim_{\mathcal J}D\cong\lim_{\mathcal I}DF.
$$