Håkon Robbestad Gylterud: Univalent Multisets

Multisets, like sets, consist of elements and the order of appearance of these elements is irrelevant. What distinguishes multisets from sets is the fact that number of occurrences of an element matters. In this talk I will show how one may capture this intuition in Martin-Löf Type Theory.

First, I will present a technical result on the identity types of W-types in type theory (without the Univalence Axiom). In light of this result I will give an analysis of the underlying type of Aczel's model of Constructive Zermelo-Fraenkel set theory (CZF) in presence of the Univalence Axiom. The conclusion is that Aczel's type, considered with the identity type as equality, consist of iterative, transfinite multisets.

I will also present an axiomatic approach to multisets - based on a "translation" of the axioms of CZF.