Local topos (source code)

= Local topos

A topos over sets is local when its <global sections functor> is itself an inverse image functor. For an idempotent-complete small indexing category, its <presheaf topos> is local exactly when the indexing category has a terminal object: then global sections are evaluation at that object.