Univalent Material Set Theory
Håkon Robbestad Gylterud, Elisabeth Stenholm
TL;DR
This work extends material set theory into the higher-type regime of HoTT by introducing ∈-structures: extensional relations between elements of a type that can themselves inhabit higher-type levels. It develops a coalgebraic perspective via the P^n_U hierarchy, proving a correspondence between extensional coalgebras and U-like ∈-structures, and constructs initial algebras V^n of P^n_U that form n-type universes of n-types with definitional decoding. The paper provides a comprehensive framework of higher-level axioms (restricted separation, replacement, union, exponentiation, etc.) unified under ∈-structures, and demonstrates fixed-point models that satisfy these axioms (except foundation), with V^n serving as an n-type universe of n-types. Formalisation in Agda underpins the results, and a clear path is laid for representing types within ∈-structures, culminating in a rigorous, scalable generalisation of material set theory within HoTT.
Abstract
Homotopy type theory (HoTT) can be seen as a generalisation of structural set theory, in the sense that 0-types represent structural sets within the more general notion of types. For material set theory, we also have concrete models as 0-types in HoTT, but this does not currently have any generalisation to higher types. The aim of this paper is to give such a generalisation of material set theory to higher type levels within homotopy type theory. This is achieved by generalising the construction of the type of iterative sets. At level 1, this gives a connection between groupoids and multisets. More specifically, we define the notion of an $\in$-structure as a type with an extensional binary type family and generalise the axioms of constructive set theory to higher type levels. Once an $\in$-structure is given, its elements can be seen as representing types in the ambient type theory. The theory has an alternative, coalgebraic formulation, in terms of coalgebras for a certain hierarchy of functors, $P^n$, which generalises the powerset functor from sub-types to covering spaces and $n$-connected maps in general. The coalgebras which furthermore are fixed-points of their respective functors in the hierarchy are shown to model the axioms given in the first part. As concrete examples of models for the theory developed we construct the initial algebras of the $P^n$ functors. In addition to being an example of initial algebras of non-polynomial functors, this construction allows one to start with a univalent universe and get a hierarchy of $\in$-structures which gives a stratified $\in$-structure representation of that universe. These types are moreover $n$-type universes of $n$-types which contain all the usual types an type formers.