Properties of Arithmetic Universes and Locoi

Abstract

In this thesis, we study two kinds of categories: locoi, which are lextensive categories with list objects, and arithmetic universes, which are pretoposes with list objects. We show three main results: first, if 𝒞 is a locos, then the list object functor 𝐿 : 𝒞 → 𝒞 is a polynomial functor. Second, if 𝒞 is a locos, then the full subcategory Fin(𝒞) of finite objects is a Boolean topos. Third, if 𝑆 is an arithmetic universe, then the free extension of 𝑆 by an object is the category [Finₛ, 𝕊] of indexed copresheaves on the internal category Finₛ of finite sets in 𝑆.