The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations
Daniel Gratzer, Håkon Gylterud, Anders Mörtberg, Elisabeth Stenholm
TL;DR
This paper constructs a strict, non-univalent universe of iterative sets $V^0$ within HoTT/UF by refining Aczel's set hierarchy using a Tarski-style universe built from $W$-types. It proves that $V^0$ is an $h$-set and can be organized as a locally cartesian closed category, with a full and faithful embedding into the category of $h$-sets, and it provides an extensional model of MLTT internal to MLTT+UA via a category-with-families structure. The work emphasizes constructivity and predicativity, avoiding HITs and quotients beyond those available in the base universe, while preserving definitional decoding of type formers and enabling formalization in Agda with agda-unimath. The results illuminate how a strict universe of $h$-sets can model the set-theoretic fragment of type theory inside HoTT/UF and connect to alternative set-universe constructions, potentially supporting internal set models, presheaf-valued variants, and cubical-style reasoning for substitution coherence.
Abstract
When working in Homotopy Type Theory and Univalent Foundations, the traditional role of the category of sets, Set, is replaced by the category hSet of homotopy sets (h-sets); types with h-propositional identity types. Many of the properties of Set hold for hSet ((co)completeness, exactness, local cartesian closure, etc.). Notably, however, the univalence axiom implies that Ob(hSet) is not itself an h-set, but an h-groupoid. This is expected in univalent foundations, but it is sometimes useful to also have a stricter universe of sets, for example when constructing internal models of type theory. In this work, we equip the type of iterative sets V0, due to Gylterud (2018) as a refinement of the pioneering work of Aczel (1978) on universes of sets in type theory, with the structure of a Tarski universe and show that it satisfies many of the good properties of h-sets. In particular, we organize V0 into a (non-univalent strict) category and prove that it is locally cartesian closed. This enables us to organize it into a category with families with the structure necessary to model extensional type theory internally in HoTT/UF. We do this in a rather minimal univalent type theory with W-types, in particular we do not rely on any HITs, or other complex extensions of type theory. Furthermore, the construction of V0 and the model is fully constructive and predicative, while still being very convenient to work with as the decoding from V0 into h-sets commutes definitionally for all type constructors. Almost all of the paper has been formalized in Agda using the agda-unimath library of univalent mathematics.