arXiv subjects

Elisabeth Stenholm

Publications and source records attributed to Elisabeth Stenholm.

3 recordsLinked to original sources

arXiv2026

Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory

Non-well-founded material sets have been modelled in Martin-Löf type theory by Lindström using setoids. In this paper we construct models of non-wellfounded material sets in Homotopy Type Theory (HoTT) where equality is interpreted as the identity type. The first model satisfies Scott's Anti-Foundation Axiom (SAFA) and dualises the construction of iterative sets. The second model satisfies Aczel's Anti-Foundation Axiom (AFA), and is constructed by adaption of Aczel-Mendler's terminal coalgebra theorem to type theory, which requires propositional resizing. In an bid to extend coalgebraic theory and anti-foundation axioms to higher type levels, we formulate generalisations of AFA and SAFA, and construct a hierarchy of models which satisfies the SAFA generalisations. These generalisations build on the framework of Univalent Material Set Theory, previously developed by two of the authors. Since the model constructions are based on M-types, the paper also includes a characterisation of the identity type of M-types as indexed M-types. Our results are formalised in the proof-assistant Agda.

math.LO↗

arXiv2024

Univalent Material Set Theory

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.

math.LO↗

arXiv2024

The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations

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.

cs.LO↗