Set-theoretic universes and paradoxes in 2-topoi

Abstract

This paper continues the development of (elementary) 2-topos theory, a foundational theory based on an axiomatization of the 2-category of categories. We prove that any 2-topos contains a model of intuitionistic ZF set theory, and we use this to show that, if appropriate size restraints are not imposed, then a Burali-Forti type paradox can be deduced from the 2-topos axioms. The set-theoretic universe is produced as a special case of a general construction giving an internal category of models in a 2-topos of an arbitrary finite higher-order theory, which in turn is carried out using a notion of "topos sketch". As a byproduct of our construction, we also make contact with the subject of "algebraic set theory", introducing a novel approach to the construction of set-theoretic universes from a "category of classes".