UNIVERSES IN TOPOSES
Thomas Streicher · 2005
Abstract This chapter discusses a notion of universe in toposes, which from a logical point of view gives rise to an extension of Higher Order Intuitionistic Arithmetic (HAH). In this way, one can construct families of types in the universe by structural recursion and quantify over such families. Further, it shows that (hierarchies of) such universes do exist in all sheaf and realizability toposes. They do not exist instead either in the free topos or in the Vω+ω model of Zermelo set theory. Though universes in the category Set are necessarily of strongly inaccessible cardinality, it remains an open question as to whether toposes with a universe allow one to construct internal models of Intuitionistic Zermelo Fraenkel set theory (IZF).