Some of you may have heard talks about my paper "Sketches for arithmetic universes", or even seen preliminary drafts of it. I now have a version which I intend to submit shortly, and have put it on my website at http://www.cs.bham.ac.uk/~sjv/AUSk.pdf I've also sent it to arXiv. The paper is intended to help deal with a problem with geometric logic, namely that it has infinities in its formalism (specifically: infinitary disjunctions) that are extrinsic to the logic itself and supplied by choosing a base topos. In practice, many of the infinities needed are countable and are not sensitive to change of base as long as the base has a natural numbers object. The aim of this work is to make those infinities intrinsic to the logic by adding type-theoretic ingredients (specifically, list objects, hence in particular nnos) that enable infinite disjunctions to be replaced by existential quantification. Categorically this amounts to replacing Grothendieck toposes (over base with nno) by arithmetic universes (no base needed) - that is to say, by pretoposes with parametrized list objects. Already, Milly Maietti has studied some type-theoretic issues for these. The paper describes "contexts", finite gadgets analogous to sketches that play the role of geometric theories, and their classifying AUs, replacing classifying toposes as generalized spaces. Maps and 2-cells for contexts are also finite gadgets. The 2-category of contexts embeds fully and faithfully in the 2-category of AUs, strict AU-functors, and natural transformations. Steve [For admin and other information see: http://www.mta.ca/~cat-dist/ ]