On toposes generated by cardinal finite objects

Abstract

We give a characterizations of toposes which admit a generating family of objects which are internally cardinal finite (i.e. Kuratowski finite and decidable) in terms of "topological" conditions. The central result is that, constructively, a hyperconnected separated locally decidable topos admit a generating family of cardinal finite objects. The main theorem is then a generalization obtained as an application of this result internally in the localic reflection of an arbitrary topos: a topos is generated by cardinal finite objects if and only if it is separated, locally decidable, and its localic reflection is zero dimensional.

arXiv comment18 pages. The logical framework has been clarified by the use of M.Shulman stack semantics. Proofs of the last section have been improved. Some typos corrected