Representable test for initial functors (source code)

= Representable test for initial functors

A <functor> $F:I\to J$ is initial if restriction preserves <categorical limits> for <diagrams in a category> with codomain $\mathbf{Set}^{\mathrm{op}}$. To test necessity, view $J(-,j)$ as such a diagram. Its limit is a singleton, since the <colimit> of the corresponding <representable presheaf> is the connected-component set of the slice $J\downarrow j$, which has a terminal object. The restricted colimit is the connected-component set of $(F\downarrow j)$. Thus that <comma category> is nonempty and connected. Sufficiency follows from <cone restriction along an initial functor>.