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öf 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.
众所周知，univalence与unique of identity proofs（UIP）是不相容的，UIP是所有类型都是h-集的公理。这是由于有限的h-集只要不是h-命题就有非平凡的自同构。一个自然的问题是，限制于h-命题的单价是否与UIP相容。我们通过构建一个模型来肯定地回答这个问题，在这个模型中，类型是同伦类型论中定义为更高归纳类型的封闭宇宙的元素。这个宇宙有一个同时“部分”单价完成的路径构造器，即，仅限于H命题。更一般地说，我们表明，单价限于$(n-1)$类型是一致的假设，所有类型的$n$截断。此外，我们参数化我们的建设一个适当的良好的行为容器，抽象从一个具体的选择类型的former的宇宙。
