From Multisets to Sets in Hotmotopy Type Theory

TL;DR

This paper constructs a model of set theory within homotopy type theory using multisets, demonstrating how univalence and set quotients can establish constructive set axioms without higher inductive types.

Contribution

It introduces a multiset-based set model in homotopy type theory that aligns with Aczel's model and leverages univalence and quotients to prove set axioms.

Findings

Model satisfies constructive set theory axioms

Equivalence with existing homotopy type theory models

Uses univalence and set quotients to establish properties

Abstract

We give a model of set theory based on multisets in homotopy type theory. The equality of the model is the identity type. The underlying type of iterative sets can be formulated in Martin-L\"of type theory, without Higher Inductive Types (HITs), and is a sub-type of the underlying type of Aczel's 1978 model of set theory in type theory. The Voevodsky Univalence Axiom and mere set quotients (a mild kind of HITs) are used to prove the axioms of constructive set theory for the model. We give an equivalence to the model provided in Chapter 10 of "Homotopy Type Theory" by the Univalent Foundations Program.