Multisets in Type Theory

TL;DR

This paper explores the concept of iterative multisets within Martin-Löf Type Theory, leveraging the Univalence Axiom to model multisets and adapt constructive set theory axioms accordingly.

Contribution

It introduces a novel model of multisets in type theory using the identity type and Univalence, extending Aczel's set-theoretic model with new foundational insights.

Findings

Model of multisets constructed using identity type and Univalence

Axioms of constructive set theory adapted to multisets hold in the model

Provides a new foundation for iterative multisets in type theory

Abstract

A multiset consists of elements, but the notion of a multiset is distinguished from that of a set by carrying information of how many times each element occurs in a given multiset. In this work we will investigate the notion of iterative multisets, where multisets are iteratively built up from other multisets, in the context Martin-L\"of Type Theory, in the presence of Voevodsky's Univalence Axiom. Aczel 1978 introduced a model of constructive set theory in type theory, using a W-type quantifying over a universe, and an inductively defined equivalence relation on it. Our investigation takes this W-type and instead considers the identity type on it, which can be computed from the Univalence Axiom. Our thesis is that this gives a model of multisets. In order to demonstrate this, we adapt axioms of constructive set theory to multisets, and show that they hold for our model.