Initial object criterion for a covariant local topos (source code)

= Initial object criterion for a covariant local topos
{title2=$[\mathcal C,\mathbf{Set}]\text{ local}\Longleftrightarrow\operatorname{Kar}(\mathcal C)\text{ has an initial object}$}

The constant singleton <functor> must be a <retract in a category> of a covariant <representable functor>. Necessity follows by applying a colimit-preserving global-sections <functor> to the canonical <coproduct> of representables onto the terminal <functor>. Conversely its Hom <functor> is a retract of evaluation, preserves <colimits> and has a <right adjoint>. Such a retract is represented by an <initial object> in the <idempotent completion>. For an idempotent-complete category an actual <initial object> suffices; without this hypothesis an absorbing-zero <monoid> gives a counterexample to the unqualified claim.