# Multisets in Type Theory

Håkon Robbestad Gylterud

###### 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öf Type Theory, in the presence of
Voevodsky’s Univalence Axiom.

[1] 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 multisets. In order to demonstrate this, we
adapt axioms of constructive set theory to multisets, and show that they hold
for our model.

###### Contents

  1. 1 Introduction
  2. 2 Notation and background
  3. 3 The model
    1. 3.1 Aczel’s model
    2. 3.2 The identity type on W-types
    3. 3.3 A model of multisets
    4. 3.4 Equality and the identity type
    5. 3.5 Extensionality
  4. 4 Multiset constructions
    1. 4.1 Restricted separation
    2. 4.2 Union-replacement
    3. 4.3 Singletons
    4. 4.4 Pairing
    5. 4.5 Ordered Pairs
    6. 4.6 Cartesian products
    7. 4.7 Functions
    8. 4.8 Fullness, subset collection and operations
    9. 4.9 Exponentiation
    10. 4.10 Natural numbers
  5. 5 Homotopic aspects of $M$
    1. 5.1 Homotopy $n$-type
    2. 5.2 HITs and multisets

##  1 Introduction

The purpose of this paper is to describe a model of iterative, transfinite
multisets and to discuss a possible axiomatisation of the model in the context
of univalent Martin-Löf style type theory. Before describing the model, we
discuss existing work on multisets and their relation to the model at hand.

Usage of multisets has a long history, both in mathematics and in
applications. In classical mathematics one models multisets inside set theory
in various ways. Here follows a brief description of three common ways of
representing multisets.

A very general definition, introduced in [9], is that a multiset on a domain
set $X$, consists of an assignment $X\rightarrow\text{Card}$, which for each
element of the domain specifies the (possibly transfinite) number of
occurrences of the element in the multiset. Often, this notion is restricted
to functions $X\rightarrow\mathbb{N}$, which represent multisets where each
element occurs finitely many times.

One can also view a multiset as a set $A$ with an equivalence relation $R$
defined on $A$. The idea is that the elements of $A$ are the occurrences in
the multiset, and the relation $R$ specifies which occurrences are the same.
Thus the number of occurrences of $a\in A$ is the size of the $R$-equivalence
class of $a$.

A third way is to consider a multiset as a family of sets. The index set of
the family corresponds to the domain in Rado’s multisets, but instead of
assigning a cardinal number, we have a set of occurrences.

These three approaches illuminate different aspects of multisets, and even
though they are formulated quite differently it is relatively easy to pass
back and forth between them. In fact they would be equivalent if one removes
the constraint that the relation in the second formulation should be
reflexive, or restricts the other two to ensure that each element in the
domain occurs at least once.

Rado’s formulation reflect that elements in a multiset occurs a specific
number of times. This can be problematic in a constructive context, where the
notion of cardinality is much more nuanced. This is solved if one takes the
family-of-sets definition, which makes perfect sense constructively, but
requires more thought as to what constitutes equality between multisets. The
notion of equality between multisets is a topic we will come back to later in
this paper.

Considering a multiset as a set with equivalence relation, a setoid, gives an
interesting way to talk about the different between identical elements and
equal elements. The identity of elements in the underlying set $A$ tells us
when occurrences are identical, and the relation $R$ tells us which
occurrences are equal. Since the underlying theory is set theory, we can
distinguish equal occurrences in a multiset, but not identical occurrences.

All three notions describe what we in this paper will refer to as “flat
multisets”, as opposed to “iterative multisets”. In a flat multiset, the
elements are taken from some domain which may not consist of other multisets.
The iterative multisets have elements which are multisets themselves, and the
collection iterative multisets is generated in a well-founded manner.

[4] develops an axiomatisation of iterative multisets with finite occurrences.
The theory is a two-sorted, first-order theory. The two sorts $N$ and $M$,
represent the natural numbers and multisets respectively. The natural numbers
are given by the Peano axioms. Membership is interpreted as a ternary
predicate $-\in_{-}-$, where the intended interpretation of $x\in_{n}y$ is
that $x$ occurs exactly $n$ times in $y$. The axioms for multisets are then
chosen so that one can reconstruct $ZFC$ internally as the multisets where
each element occurs at most once.

In this paper, we will take a different view on elementhood of multisets
compared to [4]. Instead of a ternary relation, we will keep the
${\in}$-relation binary and invoke the propositions-as-sets attitude of
Martin-Löf type theory.

In Martin-Löf type theory one does not generally distinguish the notion of set
from the notion of proposition. The notion of a set, as given by its canonical
elements, corresponds exactly to the notion of a proposition as given by its
canonical proofs. This leads us to give the binary relation ${\in}$ the typing
${\in}:M\rightarrow M\rightarrow{\operatorname{Type}}$. Thus, for given
$x,y:M$, we have that $x\in y$ is a set. _The natural interpretation is that
$x\in y$ is the set of occurrences of $x$ in $y$_.

Taking the idea of using types to capture the number of occurrences further,
we need a notion of equivalence of type. This is where Univalent Type Theory
enters the picture. Voevodsky’s univalence axiom expresses[3, gives an
exposition.] that an identity between type is exactly (equivalent to) an
equivalence. For types which are mere sets this means that two mere sets are
identified if there is a bijection between them.

The model of multisets which we present in this paper is derived from a model
of constructive set theory by [1]. The multiset model can in fact be seen as a
description of what Aczel’s model looks like through the eyes of type theory
with the Univalence Axiom.

##  2 Notation and background

The following article is set with type theory as its intended metatheory. Some
results depend on the Univalence Axiom, and are marked as such. Part of the
article is formalised in Agda [6, in the references contains a URL to the
source code of the formalisation.], in particular the more technical lemmas
leading up to the extensionality theorem and the extensionality theorem
itself. However, this article is self contained, and even the proofs for which
there exists a formalisation are here presented in usual mathematical writing.

In ways of notation we will mostly use standard type theoretical notation, but
written out as informal constructive mathematics in the style of the homotopy
type theory book[10], rather than giving formal derivations. Our notation
deviate a bit from the book in ways mentioned below. Mostly, these deviations
take us close to how type theory is written in a formal proof system, such as
Agda or Coq.

Application of functions and instantiation of dependent types are denoted by
juxtaposition — e.g. $f\,a$ or $B\,a$ — leaving a small space between the
function or type and their argument.

We use $A:{\operatorname{Type}}$ to denote that $A$ is a type.

Definitions are signified by $:=$ with the type of the term often listed on
the line above the definition. Definitional equalities are denoted by
$\equiv$.

The equality sign $=$ is used to denote various equivalence relations — each
time identified with a subscript, unless clear from the context. We will use
the notation Id for the identity type.

We follow the book[10] in the definition of equivalence of types, $A\simeq B$,
homotopy of functions, $f\sim g$, and notions such as _contractible_ , _mere
proposition_ , _mere set_ , and $n$-type. For the basic properties of these
notions we refer the reader to ([10]).

Many proofs involve showing equivalences of types, which we strive to
demonstrate, as far as possible, using chains of simpler type-algebra
equivalences, such as
$\left(\prod_{a:A}\sum_{b:B\,a}C\,a\,b\right)\simeq\left(\sum_{f:\prod_{a:A}B\,a}\prod_{a:A}C\,a\,(f\,a)\right)$.

It is is worth noting that we will consider quantifiers, such as
$\forall$,$\exists$,$\prod$ and $\sum$ to bind weakly, so that for instance
$\prod_{x:a}P\,x\rightarrow Q\,x$ disambiguates to
$\prod_{x:a}(P\,x\rightarrow Q\,x)$ rather than
$\left(\prod_{x:a}P\,x\right)\rightarrow Q\,x$. We sometimes will add the
parenthesis to emphasise this.

##  3 The model

In the section we recall Aczel’s model of constructive set theory, delve into
homotopy type theory and construct a model of multiset theory.

###  3.1 Aczel’s model

The idea behind the construction of Aczel’s $V$ type in [1] is that, given a
universe $U:{\operatorname{Type}}$ with decoding type
$T:U\rightarrow{\operatorname{Type}}$, one can construct a setoid which
captures the iteratively generated sets, where each set has an index of its
elements in $U$. An element can be listed more than once in the index of the
set. The equality relation of the setoid removes the distinction between equal
sets with different representations, making sets equal if they have the same
elements.

######  Definition 3:1.

Given a universe $U$, with decoding function
$T:U\rightarrow{\operatorname{Type}}$, let Aczel’s $V$ be the setoid defined
as follows.

$\displaystyle V:{\operatorname{Type}}$ $\displaystyle V:=W_{a:U}Ta$
$\displaystyle=_{V}:V\rightarrow V\rightarrow{\operatorname{Type}}$
$\displaystyle(\sup\ a\ f)=_{V}(\sup\ b\
g):=\left(\prod_{i:Ta}\sum_{j:Tb}(f\,i)=_{V}(g\,j)\right)\wedge\left(\prod_{j:Tb}\sum_{i:Ta}(f\,i)=_{V}(g\,j)\right)$

The way to look at a canonical element $x\equiv(\sup\ a\ f):V$ is that $a$ is
a code for the index of elements in $x$ and $f:Ta\rightarrow V$ picks out the
elements (i.e. sets) contained in $x$.

#### Remark.

Notice that the relation $=_{V}$ is $U$-small, if $U$ has $\Sigma$-types and
$\Pi$-types. That is, one can prove by W-induction that for each pair of
elements $x,y:V$, there is a code in $U$ for the type $x=_{V}y$. This is
important, since we want to use equality to construct indices for new sets.

######  Definition 3:3.

Let elementhood in Aczel’s V be defined as follows.

$\displaystyle{\in}:V\rightarrow V\rightarrow{\operatorname{Type}}$ (1)
$\displaystyle x\in(\sup\,b\,g)=\sum_{i:Tb}x=_{V}(g\,i)$ (2)

#### Remark.

Since the relation $=_{V}$ is $U$-small, it follows that the relation ${\in}$
is also $U$-small.

[1] goes on to prove that the setoid $(V,=_{V})$, with the relation ${\in}$,
is a model of Constructive Zermelo-Fraenkel set theory (CZF). In this paper,
we take a different path, and ask the question: What is the nature of elements
in $V$, without taking the quotient of $=_{V}$, and instead considering the
identity type on $V$?

As noted, a set in $V$ may have the same element listed several times, but the
equality $=_{V}$ erases the distinction between representations that just
differ by the number of times they repeat elements. However we cannot expect
the identity type to do the same. Thus, we expect that the result will be more
like multisets, possibly with the obstacle that order of elements may play a
role. As we will see, this obstacle is overcome by the _univalence axiom_.

###  3.2 The identity type on W-types

The following result is due to Nils Anders Danielsson [5, only available on-
line.]. The result characterises the W-type of a type family
$B:A\rightarrow{\operatorname{Type}}$, in terms of the identity type of $A$
and $B$, up to equivalence. The lemma does not make use of the Univalence
axiom and can be carried out in plain Martin-Löf type theory.

A technical detail is that the proof as it stands, relies on $\eta$-reduction.
The justification for this is that we take the function type in the W-type to
be the $\Pi$-type of the logical framework, in which $\eta$-reduction is
customary [7]. This is also how it is implemented in Agda. However one can
carry out the proof without appeal to the $\eta$-reduction, as
$\eta$-reduction holds up to provable equality (See page 62 of [8]).

######  Definition 3:5.

Given $A:{\operatorname{Type}}$ and $B:A\rightarrow{\operatorname{Type}}$, and
an element $x:W_{A}B$ we denote by $\bar{x}:A$, and
$\tilde{x}:B\bar{x}\rightarrow W_{A}B$ the operations given by
$\overline{(\sup\,a\,f)}\equiv a$ and $\widetilde{(\sup\,a\,f)}\equiv f$.

######  Lemma 3:6.

For any $A:{\operatorname{Type}}$ and $B:A\rightarrow{\operatorname{Type}}$,
and all $x,y:W_{A}B$, there is an equivalence

$\displaystyle{\text{Id}}_{W_{A}B}\,x\,y\simeq\sum_{\alpha:{\text{Id}}_{A}\,\overline{x}\,\overline{y}}\,{\text{Id}}\,\widetilde{x}\,(B\alpha\cdot\widetilde{y})$

###  3.3 A model of multisets

We will now present our model of transfinite, iterative multisets, given a
univalent universe $U:{\operatorname{Type}}$ with decoding function
$T:U\rightarrow{\operatorname{Type}}$. It consists of a type $M$ of multisets,
an equality relation $=_{M}$ and a relation ${\in}$, which expresses
elementhood. The type $M$ is the same $W$-type as Aczel’s $V$. The equality,
however, is logically stricter than Aczel’s equality, and, as we will show,
equivalent in a strong sense to the identity type of $M$.

######  Definition 3:7.

We define

$\displaystyle M:{\operatorname{Type}}\text{ by }$ $\displaystyle
M:=W_{a:U}Ta$

and

$\displaystyle=_{M}:M\rightarrow M\rightarrow{\operatorname{Type}}\text{ by }$
$\displaystyle(\sup\,a\,f)=_{M}(\sup\,b\,g):=\sum_{\alpha:Ta\simeq
Tb}\prod_{x:Ta}(fx)=_{M}(g\,(\alpha\,x))$

and

$\displaystyle{\in}:M\rightarrow M\rightarrow{\operatorname{Type}}\text{ by }$
$\displaystyle x\in(\sup b\,g):=\sum_{i:Tb}x=_{M}(g\,i),$

#### Remark:

Observe that if $U$ has $\Pi$-types, $\Sigma$-types and identity types, then
$=_{M}$ and $\in$ are $U$-small, just like their corresponding relations in
Aczel’s $V$.

###  3.4 Equality and the identity type

######  Theorem 3:9.

(UA) For each $x,y:M$, we have
$(x=_{M}y)\simeq\left({\text{Id}}_{M}\,x\,y\right)$.

###### Proof.

By W-induction. Assume $a,b:U$ and $f:Ta\rightarrow M$ and $g:Tb\rightarrow
M$. Then

$\displaystyle(\sup a\,f)=_{M}(\sup b\,g)$
$\displaystyle\equiv\sum_{\alpha:Ta\simeq Tb}\prod_{x:Ta}(fx)=_{M}(g(\alpha
x))$ Induction hypothesis $\displaystyle\simeq\sum_{\alpha:Ta\simeq
Tb}\prod_{x:Ta}{\text{Id}}\,(f\,x)\,(g(\alpha x))$ Definition of ${\sim}$
$\displaystyle\equiv\sum_{\alpha:Ta\simeq Tb}f\sim g\cdot\alpha$
Extensionality $\displaystyle\simeq\sum_{\alpha:Ta\simeq
Tb}{\text{Id}}\,f\,(g\cdot\alpha)$ Univalence
$\displaystyle\simeq\sum_{\alpha:a=b}{\text{Id}}\,f\,(g\cdot T\alpha)$
Previous lemma $\displaystyle\simeq{\text{Id}}\,(\sup a\,f)\,(\sup b\,g)$

∎

The following lemma is important with respect to constructing multisets from
logical formulas, in analogy to the comprehension axiom of set theory. We
assume that our universe has $+$, $\Sigma$ and $\Pi$-types, so if we can only
prove that the base relations ${=_{M}}$ and ${\in}$ also live in the universe,
then we can interpret all bounded first order formulas as families of types in
$U$, indexed by some product of $M$ with it self. Thus we have the following
lemma:

######  Lemma 3:10.

${\text{Id}}_{M}$ is essentially $U$-small, in the sense that for every
$x,y:M$ there is an code $\iota\,x\,y:U$ such that
$T(\iota\,x\,y)\simeq{\text{Id}}_{M}\,x\,y$.

###  3.5 Extensionality

In set theory, the axiom of extensionality expresses that two sets are
considered equal if they have the same elements. More precisely, two sets $x$
and $y$ are equal if for any $z$ we have that $z\in x$ iff $z\in y$. This
formulation of extensionality fails for multisets, but a very similar
extensionality axiom may be formulated.

The principle of extensionality for multisets: _Two multisets $x$ and $y$ are
considered equal if for any $z$, the number of occurrences of $z$ in $x$ and
the number of occurrences of $z$ in $y$ are in bijective correspondence (in
our symbolism: $z\in x\simeq z\in y$)._

We will now prove a strong version of this principle for our model. The
crucial part of this is summarised in the following lemmas, concerning the
fibres of functions.

######  Definition 3:11.

Given a function $f:A\rightarrow B$ we define
$\operatorname{Fibre}\,f:B\rightarrow{\operatorname{Type}}$ by
$\operatorname{Fibre}\,f\,b:=\sum_{a:A}{\text{Id}}\,(f\,a)\,b$

######  Lemma 3:12.

Given function extensionality, for any $A,B,C:{\operatorname{Type}}$, and
functions $f:A\rightarrow C$ and $g:B\rightarrow C$, the following equivalence
holds:

$\displaystyle\left(\sum_{\alpha:A\rightarrow B}g\circ\alpha\sim
f\right)\simeq\left(\prod_{c:C}\operatorname{Fibre}\,f\,c\rightarrow\operatorname{Fibre}\,g\,c\right)$
(3)

###### Proof.

We define the maps $\gamma$ and $\delta$ as follows:

$\displaystyle\gamma:\left(\sum_{\alpha:A\rightarrow B}g\circ\alpha\sim
f\right)\rightarrow\left(\prod_{c:C}\operatorname{Fibre}\,f\,c\rightarrow\operatorname{Fibre}\,g\,c\right)$
$\displaystyle\gamma\,(\alpha,\sigma)\,c\,(a,p):=(\sigma_{a},\sigma_{a}\cdot
p)$

$\displaystyle\delta:\left(\prod_{c:C}\operatorname{Fibre}\,f\,c\rightarrow\operatorname{Fibre}\,g\,c\right)\rightarrow\left(\sum_{\alpha:A\rightarrow
B}g\circ\alpha\sim f\right)$ $\displaystyle\delta\,F:=(\lambda
a.\pi_{0}(F\,(f\,a)(a,\operatorname{refl}_{a})),\lambda
a.\pi_{1}(F\,(f\,a)\,(a,\operatorname{refl}_{a})))$

Unfolding the definitions shows that
$\delta\,(\gamma\,(\alpha,\sigma))\equiv(\alpha,\sigma)$ (up to
$\eta$-reduction). Id-induction on the fibres of $f$ shows that
$\gamma\,(\delta\,F)\sim F$. Thus, by function extensionality, we have the
desired equivalence. ∎

######  Lemma 3:13.

Given function extensionality, for any $A,B,C:{\operatorname{Type}}$, and
functions $f:A\rightarrow C$ and $g:B\rightarrow C$, the following equivalence
holds:

$\displaystyle\left(\sum_{\alpha:A\simeq B}g\circ\alpha\sim
f\right)\simeq\left(\prod_{c:C}\operatorname{Fibre}\,f\,c\simeq\operatorname{Fibre}\,g\,c\right)$
(4)

###### Proof.

The proof goes by showing that the equivalence constructed in 3:12 preserves
equivalences. Since being an equivalence is a $(-1)$-type, the resulting
restriction of 3:12 to equivalences is again an equivalence.

Let $\gamma$ and $\delta$ be as in 3:12, and denote by $\gamma$’ and $\delta$’
the same construction, but with $f$ and $g$ having exchanged roles. First step
is to show that for all $\alpha:A\rightarrow B$ and $\sigma:g\circ\alpha\sim
f$, if $\alpha$ is an equivalence, then for every $c:C$ the function
$\gamma\,(\alpha,\sigma)\,c:\operatorname{Fibre}\,f\,c\rightarrow\operatorname{Fibre}\,g\,c$
is an equivalence. Let $F_{c}:=\gamma\,(\alpha,\sigma)\,c$. We construct the
inverse $F_{c}^{-1}:=\gamma^{\prime}\,(\alpha^{-1},\sigma^{\prime})$, where
$\sigma^{\prime}:f\circ\alpha^{-1}\sim g$ is the proof obtained by reversing
$\sigma\alpha^{-1}:g\circ\alpha\circ\alpha^{-1}\sim f\circ\alpha^{-1}$ and
composing with the proof that $g\circ\alpha\circ\alpha^{-1}\sim g$. That
$F_{c}^{-1}$ is indeed an inverse of $F_{c}$ can be verified by Id-induction
on the fibres of $f$ and $g$ respectively.

We then show that for all $F$ such that
$F\,c:\operatorname{Fibre}\,f\,c\rightarrow\operatorname{Fibre}\,g\,c$ is an
equivalence for all $c:C$, the function $\pi_{0}(\delta\,F):A\rightarrow B$ is
an equivalence. Let $\alpha:=\pi_{0}(\delta\,F)$. Its inverse is given by
$\alpha^{-1}:=\pi_{0}(\delta^{\prime}(F^{-1})$, and the fact that it is an
inverse of $\alpha$ stems from the fact that for any $a:A$ and $c:C$ and
$h:{\text{Id}}\,(f\,a)\,c$ we have that the transport of
$(a,\operatorname{refl}_{fa}):\operatorname{Fibre}\,f\,(f\,a)$ along $h$ is
$(a,h)$, and likewise for $g$.

∎

######  Theorem 3:14.

(UA) Given $x,y:M$, the following equivalence holds.

$\displaystyle\left(x=_{M}y\right)\simeq\prod_{z:M}\left(z\in x\simeq z\in
y\right)$ (5)

###### Proof.

From Theorem 3:9 we deduce that
$x\in(\sup\,A\,f)\simeq\operatorname{Fibre}\,x\,f$. This allows us to
reformulate the above equivalence to be an instance of Lemma 3:13.

∎

##  4 Multiset constructions

Aczel’s $V$ is a model of CZF. To mirror this we look at axioms of
constructive set theory, and attempt to find corresponding axioms for
multisets. The main observation is that definite axioms111An axiom is
_definite_ if any set it claims existence of is characterised uniquely. can be
systematically changed to axioms which makes sense for multisets, by carefully
strengthening logical equivalence, $\leftrightarrow$, to equivalence in type
theory $\simeq$. A feature of this conversion is that for the axioms below, we
can retain the constructions from Aczel’s $V$ when we prove that the changed
axioms hold for $M$.

The axioms we will have a look at are

  * •

Extensionality

  * •

Restricted separation

  * •

Union Replacement

  * •

Pairing & singletons

  * •

Infinity.

  * •

Exponentiation / Fullness

  * •

Collection.

###  4.1 Restricted separation

The axiom of restricted separation says that we can select subsets by use of
formulas, as long as they are bounded. For multisets, this corresponds to that
we may multiply the number of occurrences by the family of sets represented by
the formula, as long as the family is $U$-small.

$\displaystyle\mathtt{(RSEP)}$ $\displaystyle\forall x\exists u\forall
z\left(z\in u\leftrightarrow\left(z\in x\wedge P\right)\right)$

where $P$ is a restricted formula where $u$ does not occur freely in $P$.

The formulation of RSEP in first order logic can be translated into type
theory, given our domain $M$, replacing $\leftrightarrow$ with $\simeq$.

######  Proposition 4:1.

$\displaystyle\mathtt{(M-RSEP)}$
$\displaystyle\prod_{x:M}\sum_{u:M}\prod_{z:M}\left(z\in u\simeq\left(z\in
x\wedge T\,(P\,z)\right)\right),$

where $P:M\rightarrow U$, is a $U$-small family.

###### Proof.

Define

$\displaystyle\operatorname{Sep}:(M\rightarrow U)\rightarrow M\rightarrow M$
(6)
$\displaystyle\operatorname{Sep}\,P\,x:=\sup\,\left(\sum_{i:T\,\bar{x}}P\,(\tilde{x}\,i)\right)\,\left(\tilde{x}\circ\pi_{0}\right)$
(7)

We must show that for all $x$ and $P$, that for every $z$ we have
$z\in\operatorname{Sep}\,P\,x\simeq z\in x\wedge T\,(P\,z)$.

We have:

$\displaystyle z\in\operatorname{Sep}\,P\,x$
$\displaystyle\equiv\sum_{p:\sum_{i:T\bar{x}}T\,(P\,(\tilde{x}\,i))}\tilde{x}(\pi_{0}\,p)=_{M}z$
(8)
$\displaystyle\simeq\sum_{i:T\,\bar{x}}\sum_{q:T\,(P\,(\tilde{x}\,i))}\tilde{x}(\pi_{0}\,(i,q))=_{M}z$
(9)
$\displaystyle\equiv\sum_{i:T\,\bar{x}}\sum_{q:T\,(P\,(\tilde{x}\,i))}\tilde{x}\,i=_{M}z$
(10)
$\displaystyle\equiv\sum_{i:T\,\bar{x}}\left(T\,(P\,(\tilde{x}\,i))\wedge\tilde{x}\,i=_{M}z\right)$
(11) $\displaystyle\simeq\sum_{i:T\,\bar{x}}\left(\tilde{x}\,i=_{M}z\wedge
T\,(P\,(\tilde{x}\,i)\right))$ (12)
$\displaystyle\simeq\sum_{i:T\,\bar{x}}\left(\tilde{x}\,i=_{M}z\wedge
T\,(P\,z)\right)$ (13)
$\displaystyle\simeq\left(\sum_{i:T\,\bar{x}}\tilde{x}\,i=_{M}z\right)\wedge
T\,(P\,z)$ (14) $\displaystyle\equiv z\in x\wedge T\,(P\,z)$ (15)

∎

###  4.2 Union-replacement

In [2], the authors introduce the axiom of Union-Replacement. We use this
axiom instead of separate union and replacement axioms as it seems a more
natural construction to use. For multisets it says that if we have a family of
multisets, indexed by a multiset, we can take their multiset union.

$\displaystyle\mathtt{(UR)}$ $\displaystyle\forall a\,\left(\forall x\in
a\,\exists b\,\forall y\,\left(y\in b\leftrightarrow
Q(x,y)\right)\rightarrow\exists c\,\forall y\,\left(y\in
c\leftrightarrow\exists x\in a\,Q(x,y)\right)\right)$

Rendering this in type theory and applying the translation to multisets we
get:

######  Proposition 4:2.

$\displaystyle\mathtt{(M-UR)}$
$\displaystyle\prod_{a:M}\left(\prod_{i:T\bar{a}}\sum_{b:M}\,\prod_{y:M}\left(y\in
b\simeq Q\,(\tilde{a}\,i)\,y\right)\right)$
$\displaystyle\rightarrow\sum_{c:M}\prod_{y:M}\left(y\in
c\simeq\sum_{i:T\bar{a}}Q(\tilde{a}\,i)\,y\right)$

where $Q:V\rightarrow V\rightarrow Set$ is any relation.

###### Proof.

We define

$\displaystyle\operatorname{UnionRep}:(a:M)\rightarrow(\bar{a}\rightarrow
M)\rightarrow M$ (16)
$\displaystyle\operatorname{UnionRep}\,a\,f:=\sup\,\left(\sum_{i:T\bar{a}}\overline{(f\,i)}\right)\,\left(\lambda
p.\widetilde{f\,(\pi_{0}\,p)}\,(\pi_{1}\,p)\right)$ (17)

Let us fix $a:M$. Then, from the assumption of
$\prod_{i:T\bar{a}}\sum_{b:M}\,\prod_{y:M}\left(y\in b\simeq
Q\,(\tilde{a}\,i)\,y\right)$, we can extract $f:T\bar{a}\rightarrow M$ such
that for all $i:T\bar{a}$ and all $y:M$ we get $y\in(f\,i)\simeq
Q\,(\tilde{a}\,i)\,y$. What we then need, is to show that for every $y:M$ we
have $y\in(\operatorname{UnionRep}\,a\,f)\simeq\sum_{i\in
T\bar{a}}Q(\tilde{a}\,i)\,y$.

We have

$\displaystyle y\in(\operatorname{UnionRep}\,a\,f)$
$\displaystyle\equiv\sum_{p:\sum_{i:T\bar{a}}\overline{f\,i}}\widetilde{f\,(\pi_{0}\,p)}\,(\pi_{1}\,p)=_{M}y$
(18)
$\displaystyle\simeq\sum_{i:T\bar{a}}\sum_{j:T\overline{f\,i}}\widetilde{(f\,i)}\,j=_{M}y$
(19) $\displaystyle\equiv\sum_{i:T\bar{a}}y\in(f\,i)$ (20)
$\displaystyle\simeq\sum_{i:T\bar{a}}Q(\tilde{a}\,i)\,y$ (21)

∎

###  4.3 Singletons

In set theory, singletons are usually constructed by pairing an element with
itself. For multisets defining singletons from pairs would not work, as the
resulting multiset would contain the element twice, not once. We therefore
will prove that our model has singletons.

If we were to have a singleton axiom in set theory, it would look like:

$\displaystyle\mathtt{(SING)}$ $\displaystyle\forall a\,\exists b\,\forall
z\,\left(z\in b\leftrightarrow z=a\right)$

Which for our multisets becomes:

######  Proposition 4:3.

$\displaystyle\mathtt{(M-SING)}$
$\displaystyle\prod_{a:M}\,\sum_{b:M}\,\prod_{z:M}\,\left(z\in b\simeq
z=_{M}a\right)$

###### Proof.

We define

$\displaystyle\operatorname{Sing}:M\rightarrow M$
$\displaystyle\operatorname{Sing}\,a:=\sup\,1\,\left(\lambda i.a\right)$

and prove that for every $a,z:M$ we have
$\left(z\in\operatorname{Sing}\,a\right)\simeq\left(z=_{M}a\right)$.

$\displaystyle z\in\operatorname{Sing}\,a$
$\displaystyle\equiv\sum_{i:1}\left(\lambda i.a\right)\,i=_{M}z$ (22)
$\displaystyle\equiv\sum_{i:1}a=_{M}z$ (23) $\displaystyle\equiv
1\wedge(a=_{M}z)$ (24) $\displaystyle\simeq z=_{M}a$ (25)

∎

_Notation:_ We will from now on use the notation
$\\{a\\}:=\operatorname{Sing}\,a$.

###  4.4 Pairing

The axiom of pairing,

$\displaystyle\mathtt{(PAIR)}$ $\displaystyle\forall a\,\forall b\,\exists
c\,\forall z\,\left(z\in b\leftrightarrow\left(z=a\vee z=b\right)\right),$

becomes

######  Proposition 4:4.

$\displaystyle\mathtt{(M-PAIR)}$
$\displaystyle\prod_{a:M}\,\prod_{b:M}\,\sum_{c:M}\,\prod_{z:M}\,\left(z\in
c\simeq\left(z=_{M}a\vee z=_{M}b\right)\right)$

###### Proof.

First, define

$\displaystyle p:M\rightarrow M\rightarrow 2\rightarrow M$ (26) $\displaystyle
p\,a\,b\,(l\,*):=a$ (27) $\displaystyle p\,a\,b\,(r\,*):=b$ (28)

Then, let us define

$\displaystyle\operatorname{Pair}:M\rightarrow M\rightarrow M$
$\displaystyle\operatorname{Pair}\,a\,b:=\sup\,2\,\left(p\,a\,b\right)$

It remains to show that for all $a,b,z\in M$ we have
$z\in(\operatorname{Pair}\,a\,b)\simeq\left(z=_{M}a\vee z=_{M}b\right)$.

$\displaystyle z\in(\operatorname{Pair}\,a\,b)$
$\displaystyle\equiv\sum_{i:2}p\,i=_{M}z$ (29) $\displaystyle\simeq
p\,(l\,*)=_{M}z\vee p\,(r\,*)=_{M}z$ (30) $\displaystyle\equiv a=_{M}z\vee
b=_{M}z$ (31) $\displaystyle\simeq z=_{M}a\vee z=_{M}b$ (32)

∎

Notation: We will from now on use the notation
$\\{a,b\\}:=\operatorname{Pair}\,a\,b$.

######  Lemma 4:5.

For all $a,b,a^{\prime},b^{\prime}:M$,

$\displaystyle\\{a\\}=_{M}\\{a^{\prime}\\}$ $\displaystyle\simeq
a=_{M}a^{\prime}$ (33)
$\displaystyle\\{a,b\\}=_{M}\\{a^{\prime},b^{\prime}\\}$
$\displaystyle\simeq\left((a=a^{\prime}\wedge
b=b^{\prime})\vee(a=b^{\prime}\wedge b=a^{\prime}\right).$ (34)

#### Example

The singleton with two elements

Observe that $(\\{\emptyset,\emptyset\\}=\\{\emptyset,\emptyset\\})\simeq 2$.
This leads to the perhaps surprising fact that

$\displaystyle\left(\\{\emptyset,\emptyset\\}\in\\{\\{\emptyset,\emptyset\\}\\}\right)\simeq
2.$ (35)

This might leave us feeling a bit uneasy, as this is supposed to be a
singleton, not a “doubleton”, but we will see later (Example 5:2) how to
construct a multiset in which $\\{\emptyset,\emptyset\\}$ occurs but once, and
that this construction is somewhat like a quotient of the singleton. For the
time being we accept this slight anomaly as a consequence of our rules.

#### Remark:

Using singletons, pairs and union we can construct any finite tupling of
elements of $M$. As we see from the binary case (4:5), the induced mapping
$M^{n}\rightarrow M$ is not an embedding.

###  4.5 Ordered Pairs

In set theory there are many equivalent ways to encode ordered pairs from
unordered pairs. The most common one, the Kuratowski encoding, defines
$\langle a,b\rangle=\\{\\{a\\},\\{a,b\\}\\}$. It satisfies the characteristic
property, that for all $a,b,a^{\prime},b^{\prime}$,

$\displaystyle\langle a,b\rangle=\langle
a^{\prime},b^{\prime}\rangle\leftrightarrow\left(a=a^{\prime}\wedge
b=b^{\prime}\right)$ (36)

To understand ordered pairs of multisets, we should therefore require that for
all $a,b,a^{\prime},b^{\prime}:M$

$\displaystyle\langle a,b\rangle=\langle
a^{\prime},b^{\prime}\rangle\simeq\left(a=_{M}a^{\prime}\wedge
b=_{M}b^{\prime}\right)$ (37)

However, this is not satisfied by mimicking the Kuratowski encoding. We can
see this by letting $a=b=a^{\prime}=b=\emptyset$. Given this, we can calculate
that
$\\{\\{a\\},\\{a,b\\}\\}=_{M}\\{\\{a^{\prime}\\},\\{a^{\prime},b^{\prime}\\}\\}\simeq
2$ while $\left(a=_{M}a^{\prime}\wedge b=_{M}b^{\prime}\right)\simeq 1$.

In stead of the Kuratowski encoding, we use the older definition of [11],
$\langle a,b\rangle=\\{\\{\\{a\\},\emptyset\\},\\{\\{b\\}\\}\\}$, which
harmonises with the multiset version of the characteristic property.

###### Proof.

Observe that $\\{\\{a\\},\emptyset\\}\neq_{M}\\{\\{b\\}\\}$ and
$\\{a\\}\neq_{M}\emptyset$. So we get that

$\displaystyle\langle a,b\rangle=_{M}\langle a^{\prime},b^{\prime}\rangle$
$\displaystyle\equiv\\{\\{\\{a\\},\emptyset\\},\\{\\{b\\}\\}\\}=_{M}\\{\\{\\{a^{\prime}\\},\emptyset\\},\\{\\{b^{\prime}\\}\\}\\}$
(38)
$\displaystyle\simeq\\{\\{a\\},\emptyset\\}=_{M}\\{\\{a^{\prime}\\},\emptyset\\}\wedge\\{\\{b\\}\\}=_{M}\\{\\{b^{\prime}\\}\\}$
(39)
$\displaystyle\simeq(\\{a\\}=_{M}\\{a^{\prime}\\}\wedge\emptyset=_{M}\emptyset)\wedge(\\{b\\}=_{M}\\{b^{\prime}\\})$
(40) $\displaystyle\simeq a=_{M}a^{\prime}\wedge b=_{M}b^{\prime}$ (41)

∎

###  4.6 Cartesian products

We obtain the cartesian product of two multisets by nesting
$\operatorname{UnionRep}$ around pairing.

######  Definition 4:8.

Given $a,b:M$ define

$\displaystyle a\times b:=\operatorname{UnionRep}\,a\,(\lambda
i.\operatorname{UnionRep}\,b\,(\lambda
j.\langle\tilde{a}\,i,\tilde{b}\,j\rangle))$ (42)

Each pairing can occur multiple times in the cartesian product. To be precise
$\langle x,y\rangle\in\left(a\times b\right)\simeq\left(x\in
a\right)\times\left(y\in b\right)$.

###  4.7 Functions

There are several choices one could make as to what constitutes a function
between multisets. Just like in set theory, where a function between sets is
it self a set — namely a set of pairs — we should like functions between
multisets themselves to be multisets. Therefore, a given pair $\langle
x,y\rangle$ cannot occur an unbounded number of times in a function, as we
then would have problems collecting functions into exponential multisets.

The weakest notion of a function between two multisets is just a map of
occurrences. We will refer to this as a “multiset operation”. Often one
consider the stricter notion which sends equal occurrences to equal
occurrences. This notion we will denote by “multiset function”. As we will now
see, we can express both in our model.

In the model, the notion of a multiset operation between $\sup\,A\,f$ and
$\sup\,B\,g$ corresponds exactly to a map $\phi:A\rightarrow B$, and the
stricter notion adds the requirement that if $f\,a=_{M}f\,a^{\prime}$ then
$g\,(\phi\,a)=_{M}g\,(\phi\,a^{\prime})$. The stricter notion corresponds to
functions in Aczel’s $V$, but the weaker notion is equivalent to the stricter
notion in the case of $\sup\,A\,f$ and $\sup\,B\,g$ being sets, in the sense
of $A$ and $B$ being of type level $0$ and $f$ and $g$ being injections.
Therefore, we can consider both an extension of the notion of function to
multisets.

The question we will now entertain is: How to capture these two notions in the
kind of formulas we have so far considered for other axioms? Starting with the
operations, we remind our selves that, for iterative sets, a function
$f:A\rightarrow B$ is a subset of $A\times B$, such that the projection down
to $A$ is a bijection. Having equivalences available in our language, we can
use the fibrewise equivalence lemma222Lemma 3:13 to describe the corresponding
situation for multisets.

######  Definition 4:9.

We define the weak notion of a multiset function as follows.

$\displaystyle\operatorname{Operation}:M\rightarrow$ $\displaystyle
M\rightarrow M\rightarrow Set$
$\displaystyle\operatorname{Operation}_{a\,b}\,f:=$
$\displaystyle\left(\prod_{z}\,z\in f\rightarrow\sum_{x}\,\sum_{y}\,z=\langle
x,y\rangle\right)$ $\displaystyle\wedge$ $\displaystyle\left(\prod_{x}\,x\in
a\simeq\sum_{y}\langle x,y\rangle\in f\right)$ $\displaystyle\wedge$
$\displaystyle\left(\prod_{y}\,y\in b\leftarrow\sum_{x}\langle x,y\rangle\in
f\right)$

Observe that weakening the ${\simeq}$ to ${\leftrightarrow}$ does not give the
usual definition of a function for sets, but rather that of a total binary
relation. Total binary relations form a set in classical set theory, but in
CZF this is weakened to the subset collection axiom which states that there is
a set of total relations in which every total relation has a refinement. We
will later prove that the collection of multiset operations form a multiset,
and this should be seen a form of subset collection / fullness.

######  Definition 4:10.

We define the notion of a multiset function as follows.

$\displaystyle\operatorname{Function}:M\rightarrow M\rightarrow M\rightarrow
Set$
$\displaystyle\operatorname{Function}_{a\,b}\,f:=\operatorname{Operation}_{a\,b}\,f\wedge\prod_{x,x^{\prime},y,y^{\prime}}\,$
$\displaystyle\left(\langle x,y\rangle\in f\wedge\langle
x^{\prime},y^{\prime}\rangle\in f\right)$ $\displaystyle\rightarrow
x=x^{\prime}\rightarrow y=y^{\prime}$

###  4.8 Fullness, subset collection and operations

In constructive set theory the axiom of fullness states that for each pair of
sets $a$,$b$ there is a set of total relations from $a$ to $b$ such that any
total relation has a restriction to these. The equivalent (relative to the
rest of the axioms of CZF) axiom of subset collection is a variation of
fullness which avoids the complication of using pairs to encode relations.

$\displaystyle\mathtt{(SUB-COLL)}$ $\displaystyle\forall a,b\exists u\forall
v(\forall x\in a\exists y\in bQ(x,y)$ $\displaystyle\rightarrow\exists z\in
u(\forall x\in a\exists y\in zQ(x,y)\wedge\forall y\in z\exists x\in
aQ(x,y)))$

An unfortunate feature of the subset collection axiom is that it states the
existence of certain sets without defining them uniquely. Classically, the
sets of functions would satisfy the property of fullness. In fact, the
requirement that the set of functions satisfying the fullness property is
equivalent to the axiom of choice. This raises the question of what the
constructive nature of this set really is.

Some insight on the matter can be found by studying Aczel’s model of CZF in
type theory. There the underlying type of the subset collection set between
$\sup\,A\,f$ and $\sup\,B\,g$ is the function type $A\rightarrow B$. In other
words, the subset collection sets are sets of operations. However, the first
order language of set theory is extensional, and thus unable to exactly pin
down what an operation is, thus the sets of which the axiom claim existence
are left indefinite by the axiom itself. In this respect, the axiom for
multisets, in our language where we have borrowed the connective ${\simeq}$
from type theory, stating the existence of multisets of operations is a
refinement of collection/fullness into a definite axiom, namely
_exponentiation for operations_.

###  4.9 Exponentiation

We define the exponential of two multisets.

######  Definition 4:11.

Let $a,b:M$ be multisets and define

$\displaystyle\operatorname{Exp}\,a\,b:M$
$\displaystyle\operatorname{Exp}\,a\,b:=\sup\,(\bar{a}\rightarrow\bar{b})\,(\lambda
f.\sup\,\bar{a}\,(\lambda i.\langle\tilde{a}i,\tilde{b}(fi)\rangle))$

Next, we formulate the exponentiation axiom for multisets and prove that there
exists a multiset in our model satisfying this axiom.

######  Proposition 4:12.

$\displaystyle\mathtt{(M-EXP)}$
$\displaystyle\prod_{a:M}\,\prod_{b:M}\,\sum_{c:M}\,\prod_{z:M}\,\left(z\in
c\simeq\left(\operatorname{Operation}_{a\,b}z\right)\right)$

###### Proof.

Let $c$ be $\operatorname{Exp}\,a\,b$. Thus, we need to prove that for any
given $z:M$, there is an equivalence $\operatorname{Operation}_{a\,b}\,z\simeq
z\in\operatorname{Exp}\,a\,b$. We will give this equivalence in two steps. (A
heuristic reason for why we need to jump through a hoop here is that
$\operatorname{Operation}_{a\,b}\,z$ has three factors while
$z\in\operatorname{Exp}\,a\,b$ has two (dependent ones), and we cannot
construct the equivalence factorwise. We therefore construct a more finely
grained equivalent which maps factorwise to both.)

Step 1. The type $\operatorname{Operation}_{a\,b}\,z$ is equivalent to the
following data:

  * •

$\alpha:\bar{a}\rightarrow\sum_{x,y:M}\langle x,y\rangle\in z$

  * •

$\beta:\sum_{x,y:M}\langle x,y\rangle\in z\rightarrow\bar{b}$

  * •

$\epsilon:\alpha\circ\pi_{0}=\tilde{a}$, where $\pi_{0}:\sum_{x,y:M}\langle
x,y\rangle\in z\rightarrow M$ extracts the $x$ component.

  * •

$\delta:\beta\circ\tilde{b}=\pi_{1}$, where $\pi_{1}:\sum_{x,y:M}\langle
x,y\rangle\in z\rightarrow M$ extracts the $y$ component.

  * •

$\pi_{0}\circ\pi_{1}\circ\pi_{1}:\sum_{x,y:M}\langle x,y\rangle\in
z\rightarrow\bar{z}$, which extracts the $z$-index, is an equivalence.

This data can be succinctly expressed by the following commutative diagram:

(49)

The type $\operatorname{Operation}_{a\,b}\,z$ is a product of three factors.
The first factor is equivalent to
$\pi_{0}\circ\pi_{1}\circ\pi_{1}:\sum_{x,y:M}\langle x,y\rangle\in
z\rightarrow\bar{z}$ being an equivalence, since it says that all elements of
$z$ are pairs. The second factor is equivalent to the data $\alpha$ and
$\epsilon$ above, by the fibrewise equivalence lemma (Lemma 3:13). Similarly,
the third factor is equivalent to the data $\beta$ and $\delta$. Thus, we
conclude that $\operatorname{Operation}_{a\,b}\,z$ is indeed equivalent to the
above data.

Step 2. The data given in step 1 is equivalent to
$z\in\operatorname{Exp}\,a\,b$, which is to say that $z$ is equal to the graph
of a map $\bar{a}\rightarrow\bar{b}$.

(56)

Given the data in step 1, define $f:\bar{a}\rightarrow\bar{b}$ by
$f:=\beta\circ\alpha$. Since
$\pi_{0}\circ\pi_{1}\circ\pi_{1}:\sum_{x,y:M}\langle x,y\rangle\in
z\rightarrow\bar{z}$ is an equivalence, which makes the diagram (56) commute,
we derive that

$\displaystyle z$ $\displaystyle=\sup\,\bar{a}\,(\lambda
i.\langle\pi_{0}\,(\alpha\,i),\pi_{0}\,(\pi_{1}\,(\alpha\,i))\rangle)$ (57)
$\displaystyle=\sup\,\bar{a}\,(\lambda
i.\langle\tilde{a}\,i,\tilde{b}\,(\beta\,(\alpha\,i))\rangle)$ (58)
$\displaystyle=\sup\,\bar{a}\,(\lambda
i.\langle\tilde{a}\,i,\tilde{b}\,(f\,i)\rangle)$ (59)

which is precisely that $z$ is the graph of $f$.

In the other direction, assuming that $z=\sup\,\bar{a}(\lambda
i.\langle\tilde{a}\,i,\tilde{b}\,(f\,i)\rangle$, we observe that
$\pi_{0}\circ\pi_{1}\circ\pi_{1}:\sum_{x,y:M}\langle x,y\rangle\in
z\rightarrow\bar{z}$ is in fact an equivalence, and project the equivalence
$q:\bar{z}\simeq\bar{a}$ from the assumed equality. We then factor $f$ into
$\alpha:=(q\circ\pi_{0}\circ\pi_{1}\circ\pi_{1})^{-1}$ and $\beta:=f\circ
q\circ\pi_{0}\circ\pi_{1}\circ\pi_{1}$. The fact that the rest of the
equalities of the data hold, follows from the definition of $\alpha$ and
$\beta$ and that diagram (56) commutes.

That this construction is an equivalence is (tedious) routine verification,
from which we spare the reader.

In conclusion, combining the above two steps, we have constructed an
equivalence $\operatorname{Operation}_{a\,b}\,z\simeq
z\in\operatorname{Exp}\,a\,b$.

∎

###  4.10 Natural numbers

The natural number axiom is straightforward to translate, and the construction
is exactly the same as in Aczel’s model.

Applying the usual abbreviations $\textendash$ $S\,y\,z\equiv\forall
x\left(x\in z\leftrightarrow\left(x\in y\vee x=y\right)\right)$, which codes
the relation $z$ is the successor of $y$, and $Z\,z\equiv\forall x\ \neg x\in
z$, coding $z$ is zero $\textendash$ the axiom of infinity in set theory can
be expressed as:

$\displaystyle\mathtt{(INF)}$ $\displaystyle\exists u\forall z\left(z\in
u\leftrightarrow\left(Z\,z\vee\exists y\in u\ S\,y\,z\right)\right)$

For multisets we give similar definitions of $S$ and $Z$, in order to define
an axiom of infinitity.

$\displaystyle S\,y\,z$ $\displaystyle:=\prod_{x:M}\left(x\in z\cong\left(x\in
y+x=y\right)\right)$ $\displaystyle Z\,z$ $\displaystyle:=\prod_{x:M}\neg x\in
z$

######  Proposition 4:13.

$\displaystyle\mathtt{(M-INF)}$ $\displaystyle\sum_{u:M}\prod_{z:M}\left(z\in
u\cong\left(Z\,z+\sum_{y:M}y\in u\wedge S\,y\,z\right)\right)$

###### Proof.

The construction of a natural number object for $M$ is the same as the
construction for Aczel’s $V$. We define a sequence of multisets
$N:\mathbb{N}\rightarrow M$, by

$\displaystyle N\,0:=\emptyset$ $\displaystyle N\,(n+1):=N\,n\cup\\{N\,n\\}$

And let our natural number object be $u=\sup\,\mathbb{N}\,N$. It just remains
to observe that $u$ satisfies the condition of $\mathtt{M-INF}$

$\displaystyle z\in u$ $\displaystyle\equiv\sum_{n:\mathbb{N}}N\,n=z$
$\displaystyle\cong z=\emptyset\vee\sum_{n:\mathbb{N}}N\,(Sn)=z$
$\displaystyle\cong z=\emptyset\vee\sum_{n:\mathbb{N}}(N\,n\cup\\{N\,n\\})=z$
$\displaystyle\cong Z\,z\vee\sum_{n:\mathbb{N}}S\,(N\,n)\,z$
$\displaystyle\cong Z\,z\vee\sum_{y:M}y\in m\wedge S\,y\,z$

∎

##  5 Homotopic aspects of $M$

The previous section might seem as though not much have changed going from the
sets $V$ to the multisets $M$. In this subsection we will take a look at what
objects might be in $M$ for which, since we work with the identity type on
$M$, higher homotopies come into play. First of all, we observe that $M$ has
the same number of non-trivial levels of homotopy as $U$ has.

###  5.1 Homotopy $n$-type

Recall from the book “Homotopy Type Theory”[10] that types can be divided into
levels, according to how many times one can iterate the identity type on the
type before it becomes trivial, in the sense of being contractible. A type is
contractible if it has an element, which every other element is (uniformly)
equal to. This is captured by the following definitions.

$\displaystyle\operatorname{isContractible}(X):=\sum_{x:X}\prod_{x^{\prime}:X}x^{\prime}=x$
(60)

$\displaystyle\mathtt{is-}(-2)\mathtt{-type}\
X=\operatorname{isContractible}(X)$ (61)
$\displaystyle\mathtt{is-}(n+1)\mathtt{-type}\
X:=\prod_{x,y:X}\mathtt{is-}(n)\mathtt{-type}({\text{Id}}\,x\,y)$ (62)

######  Proposition 5:1.

$M$ has the same homotopy $n$-type as $U$.

###### Proof.

If $M$ is homotopy $n$-type, then $U$ is also homotopy $n$-type. This follows
from the fact that the following map is an embedding.

$\displaystyle\iota:U\rightarrow M$ (63) $\displaystyle\iota
a:=(\sup\,a\,(\lambda a.\emptyset))$ (64)

On the other hand if $U$ has homotopy $n$-type, then we show by $W$-induction
on $M$ that $M$ also has homotopy $n$-type.

Let $x=(\sup\,a\,f)$ and $y=(\sup\,b\,g)$, and consider ${\text{Id}}\,x\,y$.
By Lemma 3:6 we know that:

$\displaystyle
Id\,x\,y\simeq\sum_{\alpha:{\text{Id}}_{U}\,a\,b}{\text{Id}}_{Ta\rightarrow
W}f\,(B\alpha\cdot g)$ (65)

From W-induction we have the induction hypothesis that the image of $f$ has
homotopy $n$-type, and by Theorem 7.1.8 in the book[10]., we know that this
$\Sigma$-type also has homotopy $n$-type,

∎

###  5.2 HITs and multisets

If our universe has Higher Inductive Types (HITs), we can construct multisets
where the index set is a higher groupoid structure. An interesting fact is
that even if $\bar{a}$ is a higher groupoid, we can still have that $x\in a$
is $1\text{-type}$ for all $x$ .

#### Example

In Example 4:6 we saw that the singleton construction unexpectedly gave
singletons where the single element occurred twice, because of its non-trivial
equalities to itself in $M$. A solution to this is to take the connected
compontent of the element in $M$ as the index set of the singleton, instead of
just $1$, along with the inclusion into $M$. However, this requires the
connected component to be $U$-small, which the usual construction does not
guarantee. Adding that assumption, which we conjecture could hold in general
(in homotopical models), since $M$ is locally $U$-small, we can construct
singletons even for elements of $M$ with non-trivial self-identities.

For any multiset $x:M$, such that there is $t:U$ which represents the
connected component of $x$, i.e.
$\alpha:T\,t\simeq\sum_{y:M}\|x=_{M}y\|_{-1}$, we can define a the singleton
$s\,x\,t\,\alpha:=\sup\,t(\pi_{0}\circ\alpha)$. The map $\pi_{0}\circ\alpha$
is an embedding, since $\|x=_{M}y\|_{-1}$ is a mere proposition. It follows
that the fibres $y\in s\,x\,t\,\alpha$ are all propositions, and in particular
$x\in s\,x\,t\,\alpha$ is contractible.

## References

  * [1] Peter Aczel  “The Type Theoretic Interpretation of Constructive Set Theory”  In _Logic Colloquium ’77_ North–Holland, Amsterdam-New York, 1978, pp. 55–66
  * [2] Peter Aczel and Michael Rathjen  “Notes on Constructive Set Theory”, 2001
  * [3] S. Awodey, Á. Pelayo and M. A. Warren  “Voevodsky’s Univalence Axiom in homotopy type theory”  In _ArXiv e-prints_ , 2013  arXiv:1302.4731 [math.HO]
  * [4] Wayne D. Blizard  “Multiset theory.”  In _Notre Dame Journal of Formal Logic_ 30.1 Duke University Press, 1988, pp. 36–66  DOI: 10.1305/ndjfl/1093634995
  * [5] Nils Anders Danielsson  “Positive h-levels are closed under W”, 2012  URL: https://homotopytypetheory.org/2012/09/21/positive-h-levels-are-closed-under-w/
  * [6] Håkon Robbestad Gylterud  “Formalisation of iterative multisets and sets in Agda”, 2016  URL: http://staff.math.su.se/gylterud/agda/
  * [7] Per Martin-Löf  “Intuitionistic type theory” 1, Studies in Proof Theory  Bibliopolis, Naples, 1984, pp. iv+91
  * [8] B. Nordström, K. Petersson and J. M. Smith  “Programming in Martin-Löf’s Type Theory”, 1990
  * [9] Richard Rado  “The cardinal module and some theorems on families of sets”  In _Annali di Matematica Pura ed Applicata_ 102.1, 1975, pp. 135–154  DOI: 10.1007/BF02410602
  * [10] The Univalent Foundations Program  “Homotopy Type Theory: Univalent Foundations of Mathematics”  Institute for Advanced Study: homotopytypetheory.org, 2013  URL: http://homotopytypetheory.org/book
  * [11] Norbert Wiener  “A Simplification of the Logic of Relations”  In _Proceedings of Cambridge Philosophical Society_ 17, 1914, pp. 387–390