# Non-wellfounded sets in HoTT

Håkon Robbestad Gylterud  Elisabeth Bonnevier

###### Abstract

Aczel’s anti-foundation axiom (AFA) is an alternative – dual – axiom to the
usual axiom of foundation in set theory. This article constructs a model of
AFA in homotopy type theory. Like the previous model of AFA in type theory, by
Lindström (1989), we use M-types, but rather than forming a setoid, we
identify a subtype where the identity type is the correct notion of equality.
We show that this model is dual to the model previously described in the HoTT
book – being the final coalgebra, as opposed to the initial algebra, of the
powerset operation. The results presented here are being formalised in Agda as
part of a bigger project of formalising set theory on the basis of homotopy
type theory. The development repository can be found at
https://git.app.uib.no/hott/hott-set-theory and the project has homepage
https://hakon.gylterud.net/research/iterative/.

##  1 Introduction

While many set-theoretical axioms tell us how to construct new sets – such as
pairs, unions, subsets and exponentials or powersets – the axiom foundation
puts restrictions upon the sets which exist. _There are no non-wellfounded
sets._ This restriction certainly makes it easier to prove statements by
induction over all sets, but the necessity of this is put into question by the
fact that any model, even without foundation, has a class of wellfounded sets,
on which one _can_ do induction when need be.

If, on the other hand, one chooses to exclude the axiom of foundation, the
immediate question is: _What are the non-wellfounded sets?_ The other axioms
provide us no way of constructing any non-wellfounded sets, so over the years
several _anti-foundation axioms_ have been proposed, see Aczel’s book[2] for
an overview. The axioms all provide ways to construct non-wellfounded sets.

In this article we will focus on Aczel’s anti-foundation axiom, which was
first introduced by Forti and Honsell [7]. It states that for every graph one
can find a unique assignment of sets to the nodes, such that an edge in the
graph corresponds to the elementhood relation between the assigned sets. For
instance the graph with a single node and a single edge would be assigned the
unique set $x=\\{x\\}$. From this point on, we will simply refer to Aczel’s
axiom as anti-foundation or AFA. Figure 1 gives a simple example of how AFA
can be used to construct sets.

Figure 1:  The anti-foundation axiom states that for every graph there is a
unique assignment of sets to the nodes such that the elementhood relation
coincides with the edge-relation. The graph above would define the sets:
$x=\\{x,y,z\\}$ , $y=\\{x,z\\}$ and $z=\\{x\\}$.

From a categorical point of view, graphs are coalgebras for the powerset
functor, consisting of a set of nodes $X$ and a map $m:X\rightarrow P\,X$
assigning to each node the set of nodes related to it by an outgoing edge. One
way to see anti-foundation is that over the category of classes and class
functions, the class of all sets is the final coalgebra of the powerset
functor. In this sense the axiom is exactly dual to the axiom of foundation
which states that the class of sets is the initial algebra of the powerset
functor.

Another seminal work of Aczel is the construction of a model of constructive
set theory in Martin-Löf’s type theory [1]. In current type theoretical
language, his model is the W-type over the decoding family of the universe – a
type whose universal property is exactly that of being an initial algebra.
Thus, unsurprisingly, Aczel’s model satisfies the constructive version of
foundation, called $\in$-induction. Lindström [10] showed that the dual
construction of the W-type, called the M-type, could be used to obtain a model
of set theory with anti-foundation.

Both Aczel and Lindströms models use a (co-)inductively defined equivalence
relation as the equality in their model. In type theory, however, every type
comes equipped with a canonical notion of equality – called _the identity
type_. Using the univalence axiom, we can compute the identity type for
Aczel’s model. In a previous article by one of the authors [9], we observed
that because of the stricter notion of equality provided by the identity type
it makes sense to regard the underlying type of Aczel’s model as a type of
(generalised and iterative) multisets.

Chapter 10 of _Homotopy Type Theory_ [11] constructs an analogue of Aczel’s
model using a higher inductive type (HIT) to make a quotient and get the
correct identity type. An alternative construction of this type which avoids
HITs was given in [8].

In this article, our goal is to construct a model of set theory with anti-
foundation, where the equality is the identity type. The main obstacle to
overcome is defining co-inductively what it means for an element of the
M-type, $\rotatebox[origin={c}]{-180.0}{$\operatorname{W}$}_{A:U}A$, of co-
iterative types, to be a _co-iterative set_. The solution found uses the
ability to form images of functions, and the universal property of $M$-types.
For a categorical perspective on $M$-types see van den Berg and De Marchi’s
article [12], and for a proof of their existence in homotopy type theory, see
the paper and formalisation by Ahrens et al. [4].

From a organisational point of view, we can see our work as completing the
table below, by constructing a terminal coalgebra for the powerset functor,
and showing the corresponding model of set theory satisfies AFA.

Functor | Initial algebra | Terminal coalgebra
---|---|---
$X\mapsto\sum_{A:U}\left(A\rightarrow X\right)$ | Aczel 1978 | Lindström 1989
$X\mapsto\sum_{A:U}\left(A\hookrightarrow X\right)$ | V from the HoTT Book | The current work.

Our model is a restriction of a model of multisets, for which we prove a
multiset version of anti-foundation. The relationship between multisets and
non-wellfounded sets was also studied by D’Agostino and Visser [5], but from a
classical point of view with a ternary predicate $x\in_{\kappa}y$ meaning $x$
occurs $\kappa$-many times in $y$, for a cardinal $\kappa$.

###  1.1 Outline

Section 1

In the introduction we present notation and an additional assumption
assumption made on the unverse.

Section 2

This section describes the specific formulation of the axioms we will prove.
The concept of models we use here, $\in$-structures, is slightly generalised
from previous work on set theory in type theory, but our main model is of the
traditional kind where $x\in y$ is a proposition.

Central to this endeavour is the powerset operation,
$\operatorname{P}_{U}\,X:=\sum_{A:U}(A\hookrightarrow X)$, which maps a type
$X$ to the set of embeddings of small types into $X$. In fact, the rest of the
work can then be summarised in terms of $\operatorname{P}_{U}$ coalgebra as
follows:

Section 3

Every (locally $U$-small111A locally $U$-small type is a type $X$ such that
for all $x,x^{\prime}:X$ the identity type $x=x^{\prime}$ is equivalent to a
type in $U$.) fixed point of $\operatorname{P}_{U}$ (i.e. type $V$ such that
$V\simeq\operatorname{P}_{U}\,V$) gives rise to a model of constructive set
theory in which the following axioms hold:

Extensionality | Pairing
---|---
Replacement | Union
Restricted separation | Exponentiation
Empty set | Natural numbers

Section 4

The type $V^{0}_{\infty}$, defined in this secton, is a locally $U$-small,
terminal coalgebra for $\operatorname{P}_{U}$.

Section 5

For the terminal coalgebra for $\operatorname{P}_{U}$, the fixed point model
constructed in Section 3 also satisfies Anti-foundation.

This complements the construction in a previous article [8], which, from this
point of view constructs an initial algebra for $\operatorname{P}_{U}$, and
shows that it satisfies foundation.

A note about the name $V^{0}_{\infty}$: The “$\infty$”-subscript is used here
to indicate the analogy with the usual notation for co-natural numbers
$\mathbb{N}_{\infty}$, and the super script “0” indicates the h-level of the
type.

###  1.2 Notation

The notation of this paper is informal type theoretical notation, of the kind
that we find in _Homotopy Type Theory_ [11].

  * •

Types are denoted $A:\operatorname{Type}$ – we take $\operatorname{Type}$ to
be a univalent universe of large types.

  * •

The sign “$:=$” denotes definitions, and $\equiv$ for judgemental equalities.

  * •

The equality sign, “=”, is used for identity types.

  * •

$U$ is a univalent universe (of small types). We suppress the notation of the
decoding family, such that $A:U$ will entail $A:\operatorname{Type}$.

  * •

$\simeq$ denotes equivalences and $\operatorname{ua}:A\simeq B\rightarrow A=B$
is the function obtained from univalence of $U$.

  * •

$f\,a$ denotes the application of the function $f$ to the element $a$.

  * •

Composition of elements in identity types is denoted by $p\cdot q$.

  * •

$\operatorname{W}_{a:A}B\,a$ denotes the W-type inductively generated by
$\sup:\prod_{a:A}(A\rightarrow\operatorname{W}_{a:A}B\,a)\rightarrow\operatorname{W}_{a:A}B\,a$.

  * •

$\rotatebox[origin={c}]{-180.0}{$\operatorname{W}$}_{a:A}B\,a$ denotes the
M-type defined co-inductively by
$\operatorname{desup}:\operatorname{W}_{a:A}B\,a\rightarrow\sum_{a:A}(A\rightarrow\operatorname{W}_{a:A}B\,a)$.
We use a rotated $\operatorname{W}$, instead of $\operatorname{M}$ to
distinguish it from the structures denoted $M$.

  * •

$\operatorname{Fin}\,n$ denotes a specific choice of finite types, where
$\operatorname{Fin}\,n$ has $n$ elements.

  * •

$\pi_{0}:\left(\sum_{a:A}B\,a\right)\rightarrow A$ is the first projection. A
notable special case is when $B\,a$ is a proposition for all $a$, then
$\pi_{0}$ is an embedding.

  * •

$\pi_{1}:\left(\sum_{a:A}B\,a\right)\rightarrow B\,(\pi_{0}\,a)$ is the second
projection.

  * •

$A\hookrightarrow B:=\sum_{f:A\rightarrow B}\operatorname{is-prop}f^{-1}$
denotes the type of embeddings.

  * •

$A\twoheadrightarrow B:=\sum_{f:A\rightarrow B}\prod_{b:B}\exists_{a:A}f\,a=B$
is the type of surjections.

###  1.3 Images of small types – an additional assumption

Given a function $f:A\rightarrow B$ there are two ways of looking its image:
as a sub-type of $B$ or a quotient of $A$. Thinking of both simultaneously,
one obtains the image factorisation of $f$ (See Figure 2). The definition in
the HoTT book [11][p. 313] emphasises the subset-view by defining the image of
a function $f:A\rightarrow B$ as the type $\sum_{b:B}\exists_{a:A}f\,a=b$. The
quotient view can be addressed for mere sets, by using mere-set-quotients
which are well understood. But, as the following indicates, the quotient-view
is more complicated with higher types.

Figure 2: The usual diagram of image factorisation.

Taking the images of functions is an essential part of the model construction
which follows. The main concern is how constructing the image of a function
interacts with keeping track of the size, or universe level, of the types
involved.

The characterisation in the HoTT book of the image as
$\sum_{b:B}\exists_{a:A}f\,a=b$, makes it clear that if the universe is closed
under propositional truncation and the types $A$ and $B$ both reside in the
universe, then so does the image of $f$. Further more, if one assumes the
impredicative axiom that all propositions are small, then it is sufficient
that $B$ is $U$-small for the image to also be so. But if $A$ is in $U$, is it
possible to weaken the assumption that $B$ is in $U$ and still conclude that
the image is in $U$?

As a higher groupoid, the image looks like it has the objects from $A$, but
the morphisms between any two objects are the morphisms from $B$ between the
objects resulting from applying $f$. _From this intuition it seems reasonable
that if all the identity types of $B$ lie in $U$, along with $A$, then the
resulting higher groupoid image also lie in $U$._ As pointed out below, this
is not true for all univalent universes, but the results in presented here
will rely upon the assumption that this holds for our particular universe.

The formulation of this assumption relies on two natural notions of smallness.

######  Definition 1.

A type $X$ is essentially $U$-small if there is $A:U$ such that $A\simeq X$.
That is, $\sum_{A:U}A\simeq X$.

######  Lemma 1.

Being essentially $U$-small is a mere proposition.

###### Proof.

We must show that the type $\sum_{A:U}A\simeq X$ is a mere proposition. This
type looks close to being of the form $\sum_{b:T}b=a$, which is known to be
contractible, but $X$ is not a type in the universe we cannot directly apply
univalence. Instead we give a direct proof based on the definition of being a
mere proposition.

Let $(A,\alpha)$ and $(B,\beta)$ be two elements of $\sum_{A:U}A\simeq X$.
Applying univalence, we observe that
$\operatorname{ua}(\beta^{-1}\cdot\alpha):A=B$.

It remains to show that we get $\beta$ by transporting $\alpha$ along the path
$\operatorname{ua}(\beta^{-1}\cdot\alpha)$, in the family
$\lambda(Y:U).Y\simeq X$. But this is easily computed with path algebra:

$\displaystyle\operatorname{tr}^{\lambda Y.Y\simeq
X}_{\operatorname{ua}(\beta^{-1}\cdot\alpha)}\alpha$
$\displaystyle=\alpha\cdot(\beta^{-1}\cdot\alpha)^{-1}$ (1)
$\displaystyle=\alpha\cdot\alpha^{-1}\cdot\beta$ (2) $\displaystyle=\beta$ (3)

∎

######  Definition 2.

A type $X$ is locally $U$-small if for each $x,x^{\prime}:X$ the identity type
$x=x^{\prime}$ is essentially $U$-small.

Now, the following assumption, which will be assumed throughout the paper, can
be formulated:

######  Assumption 1 (Images of small types).

For every small type $A:U$ and every locally small $X:Type$, and given a
function $f:A\rightarrow X$, there is a small type
$\operatorname{image}\,f:U$, and functions
$\operatorname{surj}f:A\twoheadrightarrow\operatorname{image}\,f$ and
$\operatorname{incl}f:\operatorname{image}\,f\hookrightarrow X$, such that for
every $a:A$ we have $\operatorname{incl}f(\operatorname{surj}f\,x)\equiv
f\,x$.

Remark: Not all univalent universes satisfy the above assumtion. For instance,
given any univalent universe, $U$, we can define the subuniverse of mere sets,
$\operatorname{Set}_{U}$. This subuniverse is univalent, and locally
$\operatorname{Set}_{U}$-small, but the image of the map $(\lambda
x.2):1\rightarrow\operatorname{Set}_{U}$ is not a set: there is a non-trivial
equality $2=2$, arising from negation. Thus, the image of this map is not
essentially $\operatorname{Set}_{U}$-small.

While the work in this article is presented informally in type theory, there
might be some benefit here to spell out the assumption as formulated in Agda.
This formulation is uniform in universe levels (the parameters i and j) so
that it can applied at any level.

    module _ {i j}
             {Domain : Type i} {Codomain : Type j}
             (_ : LocallySmall i Codomain)
             (f : Domain  Codomain) where

      postulate Image : Type i

      postulate image-inclusion : Image  Codomain

      postulate image-quotient : Domain  Image

      postulate image- :  x  (image-inclusion  image-quotient  x  )  f x

      {-# REWRITE image- #-}

This code can be found in the repository at https://git.app.uib.no/hott/hott-
set-theory, where the file containing the above snippet is called
“Function/ImageFactorisation.agda”.

###  1.4 $U$-Powersets

The model of AFA which we will construct is an example of a fixed point, in
fact a terminal coalgebra, of the following restricted powerset operation:

######  Definition 3.

We define the $U$-powerset operation, which maps a type to the type of its
$U$-small subtypes, by $\operatorname{P}_{U}\,X:=\sum_{A:U}A\hookrightarrow
X$.

This definition of powerset is different from the one in the book “Homotopy
Type Theory” [11, p. 151], which – by assuming propositional resizing – is not
relative to a specific universe. It is also different, apriori, when not
assuming propositional resizing, from the set
$X\rightarrow\operatorname{Prop}_{U}$.

######  Lemma 2 (Equality in powersets is fiberwise).

For any type $X$, and any $U,V:\operatorname{P}_{U}\,X$ we have that
$(U=V)\simeq\prod_{x:X}((\pi_{1}\,U)^{-1}x\simeq(\pi_{1}\,V)^{-1}x)$.

###### Proof.

Let $U\equiv(A,f)$ and $B\equiv(B,g)$ be two canonical elements of
$\operatorname{P}\,X$. We get a chain of equivalences using the usual
characterisation of equality in $\Sigma$-types (4), the univalence axiom (5)
and the fiberwise equivalence lemma (6)222Lemma 5 of “Multisets in Type
Theory” [9]:

$\displaystyle(A,f)=(B,g)$
$\displaystyle\simeq\sum_{\alpha:A=B}g\circ(\operatorname{coe}\,\alpha)=f$ (4)
$\displaystyle\simeq\sum_{\alpha:A\simeq B}g\circ\alpha=f$ (5)
$\displaystyle\simeq\prod_{x:X}(f^{-1}x\simeq g^{-1}x)$ (6)

∎

######  Lemma 3 (The powerset is a set).

For any type $X$, the $U$-powerset $\operatorname{P}_{U}\,X$ is a set.

###### Proof.

Let $(A,f)$ and $(B,g)$ be two canonical elements of $\operatorname{P}\,X$, we
show that $(A,f)=(B,g)$ is a proposition. We compute, using 2,
$((A,f)=(B,g))\simeq\prod_{x:X}(f^{-1}x\simeq g^{-1}x)$. Since $f$ and $g$ are
both embeddings, their fibres are proposition, hence
$\prod_{x:X}f^{-1}\,x\simeq g^{-1}\,x$ is also a proposition.∎

For it to make sense to talk about $\operatorname{P}_{U}$-coalgebras and
homomorphisms between them, the operation must be functorial. The restricted
powerset operation is functorial in the sense that it can be extended to
functions by taking images. Since the resulting image must be a type in $U$,
we are restricted to functoriality on locally $U$-small types, where we can
apply Assumption 1.

######  Definition 4.

Given $X,Y:\operatorname{Type}$, where $Y$ is locally $U$-small, and a
function $f:X\rightarrow Y$, we define
$\operatorname{P}_{U}\,f:\operatorname{P}_{U}\,X\rightarrow\operatorname{P}_{U}\,Y$
by $\operatorname{P}_{U}\,f\,(A,i):=\operatorname{image}\,(f\circ
i),\operatorname{incl}\,(f\circ i)$.

######  Definition 5 (Powerset coalgebra).

A $\operatorname{P}_{U}$-coalgebra is a pair $(X,m)$ where $X:Type$ and
$m:X\rightarrow\operatorname{P}_{U}\,X$.

######  Definition 6 (Powerset coalgebra homomorphism).

Given two $\operatorname{P}_{U}$-coalgebras $(X,m)$ and $(Y,n)$, where $Y$ is
locally $U$-small, a homomorphism from $(X,m)$ to $(Y,n)$ is a function
$f:X\rightarrow Y$ such that $n\circ f=\operatorname{P}_{U}f\circ m$.

######  Definition 7 (Terminal powerset coalgebra).

A $\operatorname{P}_{U}$-coalgebra $(Y,n)$ is terminal if $Y$ is locally
$U$-small and for every $(Y,n)$, where $Y$ is locally $U$-small, a
homomorphism from $(X,m)$ to $(Y,n)$ is a function $f:X\rightarrow Y$ such
that $n\circ f=\operatorname{P}_{U}f\circ m$.

The standard argument that the terminal coalgebra is unique applies also here.
Theorem 8 establishes that this terminal coalgebra exists.

##  2 $\in$-structures

This section sets up the framework we will use to describe the model and
define the properties the model will satisfy. First of all, we will define
what we mean with an $\in$-structure, which is here slightly different from
previous usage333For instance, in a previous article by the first author [8],
by incorporating extensionality and generalising to higher h-levels. Then we
will give formulations of the standard properties of $\in$-structures.

Zermelo—Fraenkel (ZF) set theory arose from the ashes of Cantor’s set theory
which had been set ablaze by Russel’s paradox. ZF is a formal theory in the
language of first-order logic, intended as a formal foundation for
mathematics. The fear of inconsistency necessitated a formal theory, which
could be reasoned about meta-mathematically.

In contrast, Aczel’s work on the Anti-Foundation Axiom[2], is explicitly
informal and developed in ordinary mathematical language, although nominally
set in ZF-, the ZF axioms with the axiom of foundation removed.

In what follows, we work within the framework of (informal) homotopy type
theory. From this vantage point we will try to regard set theory in the same
way that a classical mathematician regards group theory. Namely, we study a
certain type of mathematical structures, and interest ourselves in their
properties and relationships. The structures we study are not groups, but what
we call $\in$-structures: types with an extensional elementhood relation. And
just as a group theorist usually does not think of properties of groups in
terms of formulas of first-order logic, neither shall we think of properties
of $\in$-structures in these terms.

######  Definition 8.

An $\in$-structure is a pair $(M,\in)$ where $M:\operatorname{Type}$ and
$\in:M\rightarrow M\rightarrow\operatorname{Type}$, which is extensional: for
each $x,y:M$, the canonical map $x=y\rightarrow\prod_{z:M}{z\in x}\simeq{z\in
y}$ is an equivalence of types.

The usual notion of (extensional) model of set theory corresponds to
$\in$-structures, $(M,\in)$, where $x\in y$ is a mere proposition for each
$x,y:M$ (and consequently $M$ is a mere set). The model we construct at the
end of this paper, $V_{\infty}^{0}$ is of this kind. However, there are
examples of extensional $\in$-structures where $M$ is not a mere set. One such
example, based on Aczel’s[1] type $\operatorname{W}_{A:U}A$, was explored in
an article by one of the authors[9]. And in the current work we shall take the
dual type, $\rotatebox[origin={c}]{-180.0}{$\operatorname{W}$}_{A:U}A$,
originally defined by Linström[10], as our starting point when we construct
the model of AFA.

###  2.1 Ordered pairing

Since we are working in homotopy type theory, a more important distinction
than weather something can be formulated in first order logic, will be the
h-level of the properties and structures we consider.

An elementary example of this is the fact that that pairing (i.e. forming
elements $\\{a,b\\}$) is a mere proposition, while ordered pairing is a
structure: using unordered pairing, there are several ways to give an
$\in$-structure such an ordered paring-structure. Here, we will not commit to
any specific way of forming ordered pairs, but simply assume ordered pairing
as an extra structure.

######  Definition 9.

Given an $\in$-structure, $(M,\in)$, an ordered pairing structure on $(M,\in)$
is a function $\langle-,-\rangle:M\rightarrow M\rightarrow M$ such that for
every $a,b,a^{\prime},b^{\prime}:M$ the canonical map $a=a^{\prime}\times
b=b^{\prime}\rightarrow\langle a,b\rangle=\langle
a^{\prime},b^{\prime}\rangle$ is an equivalence.

######  Lemma 4.

Being an ordered pair is a mere proposition: For a fixed $\in$-structure
$(M,\in)$ with ordered pairing structure $\langle-,-\rangle$, the predicate
$\lambda(x:M).\sum_{a,b:M}\langle a,b\rangle=x$ is merely propositional.

###### Proof.

We must show that for every $x:M$ we that $\sum_{a,b:M}\langle a,b\rangle=x$
is a mere proposition. Let $((a,b),\alpha)$ and
$((a^{\prime},b^{\prime}),\beta)$ be two of its elements. Clearly
$\beta^{-1}\cdot\alpha:\langle a,b\rangle=\langle
a^{\prime},b^{\prime}\rangle$, hence $(a,b)=(a^{\prime},b^{\prime})$.
Transporting $\alpha$ along this equality we obtain $\beta$ by the usual
transport gymnastics. Thus we have that
$((a,b),\alpha)=((a^{\prime},b^{\prime}),\beta)$.∎

###  2.2 Properties for $\in$-structures

In this subsection we explicate the properties which our model is going have.
We have chosen here slightly non-standard formulations of the set theoretical
axioms – making them more native to Homotopy Type Theory. However, the ones
not prefixed “multiset” are equivalent to their usual first-order formulation.

####  2.2.1 Restricted separation

In constructive set theory, restricted separation is the ability to form sets
of the form $\\{z\in x\,\mid\,\Phi\,z\\}$, for a formula $\Phi$ where all
quantifiers are bounded (i.e. $\forall a\in b\cdots$ and $\exists a\in
b\cdots$). The usual way to internalise this to type theory is to require that
$\Phi:M\rightarrow\operatorname{Prop}_{U}$ is a predicate of propositions in
$U$.

######  Definition 10.

An $\in$-structure, $(M,\in)$, has restricted separation if for every $x:M$
and $P:M\rightarrow\operatorname{Prop}_{U}$ there is $u:M$ such that
$\prod_{z:M}z\in u\simeq((z\in x)\times P\,x$.

####  2.2.2 Pairing and unordered tuples

In usual set theory the axiom of pairing let us form sets from finite lists
$\\{x_{0},\cdots x_{n-1}\\}$ from the empty set by iteration:
$\\{x_{0},\cdots,x_{n}\\}={\cup}\\{\\{x_{0},\cdots
x_{n-1}\\},\\{x_{n},x_{n}\\}\\}$. We will instead form $n$-tuples uniformly:

######  Definition 11.

An $\in$-structure, $(M,\in)$, has finite, unordered tupling if for every
finite type $A$ and every vector $v:A\rightarrow M$ there is $\\{v\\}:M$ such
that for every $z:M$ we have $z\in\\{v\\}\simeq\exists_{a:A}v\,a=z$.

The empty set is the nullary unordered tuple.

Since tupling is a proposition, for any given $\in$-structure it is sufficient
to prove the existence of $\\{v\\}$ for every
$v:\operatorname{Fin}n\rightarrow M$ to show that it has tupling.

####  2.2.3 Union-replacement

Union-replacement is an axiom of set theory, introduced by Aczel and
Rathjen[3], which combines the union and replacement axioms into one. This is
very natural from a type theoretic point of view, since the $\Sigma$-type does
the heavy lifting in both. The idea is that we can form sets of the form
$\bigcup_{x\in u}f\,x$ for any class function $f$ defined on all elements of
$u$:

######  Definition 12.

An $\in$-structure, $(M,\in)$, has union-replacement if for any $u:M$ and
$r:\prod_{x:M}x\in u\rightarrow M$ there is $v:M$ such that $z\in
v\simeq\exists_{x:M}\exists_{i:x\in u}r\,x\,i=z$

####  2.2.4 Exponentiation

We use the definition of an operation from “Multisets in type theory” [9], in
order to define exponentiation. For propositional $\in$-structures, this is
equivalent to the usual definition of function.

######  Definition 13.

Given an $\in$-structure, $(M,\in),$ with an ordered pairing function,
$\langle-,-\rangle$, we define $\operatorname{operation}:M\rightarrow
M\rightarrow M\rightarrow\operatorname{Type}$ by

$\displaystyle\operatorname{operation}\,a\,b\,f$
$\displaystyle:=\left(\prod_{e:M}e\in f\rightarrow\sum_{x,y:M}e=\langle
x,y\rangle\right)$ $\displaystyle\times\left(\prod_{x:M}x\in
a\simeq\sum_{y:M}\langle x,y\rangle\in f\right)$
$\displaystyle\times\left(\prod_{y:M}(\sum_{x:M}\langle x,y\rangle\in
f)\rightarrow y\in f\right)$

######  Definition 14.

An $\in$-structure, $(M,\in)$, has exponentiation if for every $a,b:M$ there
is $a\Rightarrow b:M$ such that $\prod_{z:M}((f\in a\Rightarrow
b)\simeq\operatorname{operation}\,a\,b\,f)$.

####  2.2.5 Accessible elements and foundation

We choose the same approach as _Homotopy Type Theory_[11][10.3] to
wellfoundedness, namely accessiblity predicates.

######  Definition 15.

Given an $\in$-structure, $(M,\in)$, define inductively the predicate
$\operatorname{Acc}:M\rightarrow\operatorname{Type}$ by

  * •

$\operatorname{acc}:\prod_{x:M}(\prod_{y:M}y\in
x\rightarrow\operatorname{Acc}y)\rightarrow\operatorname{Acc}x$

A $\in$-structure, $(M,\in)$, is wellfounded if
$\prod_{x:M}\operatorname{Acc}x$.

######  Lemma 5.

For every $x:M$ the type $\operatorname{Acc}x$ is a mere proposition.

######  Definition 16.

We define $\operatorname{WF}_{M,{\in}}:=(\sum_{x:M}\operatorname{Acc}x,\lambda
xy.\pi_{0}\,x\in\pi_{0}\,y)$, the sub-$\in$-structure of accessible elements
of $(M,{\in})$.

####  2.2.6 Natural numbers

Natural numbers are defined in the usual way using the successor operation
$x\mapsto x\cup\\{x\\}$. But perhaps surprisingly, having a natural number set
is not a proposition – unless one adds the condition that it is accessible.
This is illustrated with the example below.

For clarity, the formulation below uses union and empty-set in the formulation
– even though one could formulate an equivalent definition without assuming
them.

######  Definition 17.

A natural number set in $(M,\in)$ is an object, $n:M$, such that for all $u:M$
there is an equivalence $u\in n\simeq(u=\emptyset\vee\exists_{v\in
n}u=v\cup\\{v\\})$.

The usual proof of uniqueness of the natural numbers in well-founded set
theory gives the following:

######  Lemma 6.

For a structure $(M,\in)$, having an accessible natural number set is a
proposition.

Using restricted separation, one can take any natural number set and restrict
to its accessible elements. Thus, if we have a natural number set, we get an
accessible one. However, we shall see that if anti-foundation implies the
existence of at least one other natural number set.

######  Example 1.

Assume that we have a Quine atom: an $x:M$ such that $x=\\{x\\}$. Such a set
is going to be uniquely defined by anti-foundation later. The Quine atom has
the property that $x=x\cup\\{x\\}$. The element $x$ is thus a fixed point of
the successor operation. If assume $n$ to be a well-founded natural number
set, then the set $n^{\prime}=n\cup x$ is also a natural number set, since $x$
is also a successor of an element of $n^{\prime}$ – namely itself.
Furthermore, $n^{\prime}$ is distinct from $n$, and thus having a natural
number set is not a proposition.

####  2.2.7 Graphs, decorations and anti-foundation

A graph is a set of edges. For simplicity we will use the underlying type of
elements in a given $\in$-structure as a universe of nodes. In this way, we do
not have to specify the set of nodes, and can simplify the formulation of
anti-foundation a bit.

######  Definition 18.

Given an $\in$-structure, $(M,\in)$, with an ordered paring structure,
$\langle-,-\rangle:M\rightarrow M\rightarrow M$, we say that a element $g:M$
is a graph if every element of $g$ is a pair – that is $\prod_{e:g}e\in
g\rightarrow\sum_{a,b:M}e=\langle a,b\rangle$.

Since being a pair is a proposition, the graphs form a subtype of $M$.

Next we will observe that there are two reasonable generalisations of the
anti-foundation axiom to general $\in$-structures. Informally, the anti-
foundation axiom says that any graph has a unique decoration – where a
decoration is an assignment of nodes to the set such that elements of the set
coincide with successor nodes in the graph.

The question is, given the graph such as $g=\\{\langle x,y\rangle,\langle
x,z\rangle\\}$, illustrated in 3, and an assignment $d$ weather the type
$(d\,y\in d\,x)$ should have one or two elements. At first it might seem like
the reasonable answer is _one_ since $\langle x,y\rangle\in g$ has one
element. But since $y$ and $z$ are _bisimilar_ in $g$, they will be assigned
to the same element by $d$, so there are in fact two edges in $g$ from $x$ to
a representation of $d\,y$, namely $\langle x,y\rangle$ and $\langle
x,z\rangle$. So, two coherent answers to this question are that either we
count the edges to each bisimilar node or we truncate to make $\in$ a
propositional relation.444We could also imagine that we restrict the graphs to
those which are coherent multiplicities with respect to bisimilation, but we
will not explore that direction here.

$\textstyle{x\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{y}$$\textstyle{z}$
Figure 3: The two nodes $y$ and $z$ are (trivially) bisimilar in this graph,
since they are both without any out-arrows.

######  Definition 19.

An $\in$-decoration of a graph $g$ is a map $d:M\rightarrow M$ such that for
all $x,z:M$ we have an equivalence $z\in d\,x\simeq\sum_{y:M}(\langle
x,y\rangle\in g)\times(d\,y=z)$

######  Definition 20.

An propositional $\in$-decoration of a graph $g$ is a map $d:M\rightarrow M$
such that for all $x,z:M$ we have an equivalence $z\in
d\,x\simeq\exists_{y:M}(\langle x,y\rangle\in g)\times(d\,y=z)$

######  Definition 21.

Given an $\in$-structure, $(M,\in)$, with an ordered paring structure,
$\langle-,-\rangle$, we say that it satisfies multiset anti-foundation if
every graph, $g$, has a unique decoration. That is, the type
$\sum_{d:M\rightarrow M}\prod_{x,z:M}\left(z\in d\,x\simeq\sum_{y:M}(\langle
x,y\rangle\in g)\times(d\,y=z)\right)$ is contractible.

######  Definition 22.

Given an $\in$-structure, $(M,\in)$, with an ordered paring structure,
$\langle-,-\rangle$, we say that it satisfies anti-foundation if every graph,
$g$, has a unique propositional decoration. That is, the type
$\sum_{d:M\rightarrow M}\prod_{x,z:M}\left(z\in
d\,x\simeq\exists_{y:M}(\langle x,y\rangle\in g)\times(d\,y=z)\right)$ is
contractible.

###  2.3 U-likeness

In this subsection we review the relationship between $\in$-structures and
coalgebras for the polynomial functor $X\mapsto\sum_{A:U}(A\rightarrow X)$.
Furthermore, we see that models of propositional set theory are exactly
“injective” coalgebras $M\hookrightarrow\operatorname{P}_{U}\,M$.

These are direct analogues of the classical, set-theoretical view of set-like
relations as coalgebras in the category of classes for the power-class
operation. But we include them to provide some additional motivation for the
model we construct later: Since it is the terminal
$\operatorname{P}_{U}$-coalgebra, any propositional $\in$-structure will have
a map into it!

######  Definition 23.

Given an $\in$-structure, $(M,\in)$, we define the family
$\operatorname{E}:M\rightarrow\operatorname{Type}$ by
$\operatorname{E}a=\sum_{x:M}x\in a$.

######  Definition 24.

An $\in$-structure, $(M,\in)$ is $U$-like if $\operatorname{E}a$ is
essentially $U$-small for every $a:M$. To simplify notation, we will coerce
$\operatorname{E}a:U$ in $U$-like $\in$-structures.

######  Lemma 7 ($\in$-structures are coalgebras).

For a fixed $M$, a $U$-like $\in$-structure on $M$ is equivalent to having a
coalgebra structure $M\hookrightarrow\sum_{A:U}(A\rightarrow M)$, which is an
embedding.

###### Proof.

$\displaystyle M\rightarrow\sum_{A:U}(A\rightarrow M)$
$\displaystyle\simeq\left(M\rightarrow\sum_{F:M\rightarrow\operatorname{Type}}\sum_{E:U}\left(\sum_{b:M}F\,b\right)\simeq
E\right)$ (7) $\displaystyle\simeq\sum_{\in:M\rightarrow
M\rightarrow\operatorname{Type}}\prod_{a:M}\sum_{E:U}\left(\sum_{b:M}a\in
b\right)\simeq E$ (8)

The equivalence (7) follows by substituting $\sum_{A:U}(A\rightarrow M)$ with
the equivalent type
$\sum_{F:M\rightarrow\operatorname{Type}}\sum_{E:U}(\sum_{b:M}F\,b)\simeq E$,
since a fibration $A\rightarrow M$, with a total type $A:U$ is equivalent to a
family over $M$ with $U$-small total type E. Since being $U$-small is a mere
proposition. The equivalence (8) is essentially currying.

The type $\sum_{\in:M\rightarrow
M\rightarrow\operatorname{Type}}\prod_{a:M}\sum_{E:U}\left(\sum_{b:M}a\in
b\right)\simeq E$ is exactly the type of $\in$-structures on $M$ which are
$U$-like, except for the extensionality requirement. But it can be easily seen
that the coalgebra being injective is equivalent to the corresponding
structure satisfying extensionality.∎

######  Definition 25.

Given a $U$-like $\in$-structure, $(M,\in)$, we define the element coalgebra
of $(M,\in)$,
$\operatorname{R}_{M,\in}:M\hookrightarrow\sum_{A:U}(A\rightarrow M)$ by
$\operatorname{R}_{M,\in}a:=(\operatorname{E}a,\pi_{0})$. (Again, the fact
that it is an embedding follows from extensionality)

######  Lemma 8.

Given a $U$-like $\in$-structure, $(M,\in)$, the following are equivalent:

  1. 1.

$a\in b$ is proposition for all $a,b:M$.

  2. 2.

$\operatorname{R}_{M,\in}$ restricts to a map
$M\hookrightarrow\sum_{A:U}A\hookrightarrow M$.

###### Proof.

The fibres of $\pi_{0}:(\sum_{b:M}a\in b)\rightarrow M$ are exactly types
$a\in b$.∎

The follow theorem combines the two previous lemmas in order to characterise
$\in$-structures of various $h$-levels in terms of coalgebras.

######  Theorem 1.

For a fixed $M$, a $U$-like $\in$-structure on $M$ such that $a\in b$ is an
$n$-type for all $a,b:M$ is equivalent to having a coalgebra structure
$M\hookrightarrow\sum_{A:U}(A\hookrightarrow M)$.

###### Proof.

Simple corollary of the previous two lemmas.∎

##  3 Fixed-point models

In this section we show that any locally $U$-small fixed point of
$\operatorname{P}_{U}$ can be made into a propositional $\in$-structure with
the propositional variants of the following:

  * •

restricted separation,

  * •

union-replacement

  * •

finite tupling,

  * •

exponentiation and

  * •

natural numbers.

The results in this section are very similar to the ones found in the
article[8, section §6] on constructing the iterative hierarchy as a subtype of
multisets. The observation here is that some of these hold for any fixed-point
of $\operatorname{P}_{U}$, not just the specific one constructed there. The
formalisation of these results can be found in the file
SetTheory/Model/FixedPoint.agda of the repository at
https://git.app.uib.no/hott/hott-set-theory.

We assume in this section that we are given a locally $U$-small type $V$, and
an equivalence $\sup:\operatorname{P}_{U}V\simeq V$. Since $\sup$ is an
equivalence, we can assume without loss of generality that any element $x:V$
is of the form $x\equiv\sup(A,f)$, where $A:U$ and $f:A\hookrightarrow V$.
Also note that $V$ is a set, since $\operatorname{P}_{U}V$ is (by 3).

The two main examples of locally $U$-small fixed points of
$\operatorname{P}_{U}$ are the initial $\operatorname{P}_{U}$-algebra (the
cumulutative hierarchy), and the terminal $\operatorname{P}_{U}$-coalgebra
which is constructed in Section 4.

######  Lemma 9.

The type $V$ is a set.

###### Proof.

$V\simeq\operatorname{P}_{U}V$ and $\operatorname{P}_{U}V$ is a set.∎

######  Definition 26 (Membership).

Given $x:V$ and $y\equiv\sup(A,f):V$, we define $x\in y:\operatorname{Prop}$
by $x\in y:=f^{-1}\,x\equiv\sum_{a:A}f\,a=x$ – which is a proposition since
$f$ is an embedding. Note that since $V$ is locally $U$-small, $x\in y$ is
essentially $U$-small.

######  Theorem 2 (Extensionality).

The type $V$ and the relation $\in$ forms an $\in$-structure. That is, $\in$
is extensional, in the sense that the canonical map
$x=y\rightarrow\prod_{z:V}(z\in x)\simeq(z\in y)$ is an equivalence.

###### Proof.

Since the types $x=y$ and $\prod_{z:V}(z\in x)\simeq(z\in y)$ are
propositions, any equivalence will do. Let $x\equiv\sup(A,f)$ and
$y\equiv\sup(B,g)$, then we compute by 2:

$\displaystyle(x=y)$ $\displaystyle\simeq((A,f)=(B,f))$
$\displaystyle\simeq\prod_{z:V}(f^{-1}z)\simeq(g^{-1}z)$
$\displaystyle\simeq\prod_{z:V}(z\in\sup(A,f))\simeq(z\in\sup(B,g))$
$\displaystyle\equiv\prod_{z:V}(z\in x)\simeq(z\in y)$

∎

######  Theorem 3 (Restricted separation).

$(V,\in)$ has restricted propositional separation.

###### Proof.

Given $x\equiv\sup(A,f)$ and $P:V\rightarrow\operatorname{Prop}_{U}$ we let
$u:=\sup(\sum_{a:A}P\,a,f\circ\pi_{0})$, where f$\circ$$\pi$0 is an embedding
since both $f$ and $\pi_{0}$ are. It then follows that $z\in
u\simeq\sum_{a:A}(P\,a\times(f\,a=z))\simeq P\,z\times\sum_{a:A}f\,a=z\simeq
P\,z\times z\in x$.∎

######  Theorem 4 (Union-replacement).

$(V,\in)$ has propositional union–replacement.

###### Proof.

Given $u\equiv\sup(A,f)$ and $r:\prod_{x:V}x\in u\rightarrow V$, let
$\phi:A\rightarrow V$ be given by $\phi a\rightarrow
r\,(f\,a)(a,\operatorname{refl})$ and let
$v:=\sup(\operatorname{image}\phi,\operatorname{incl}\phi)$, which has the
desired property.∎

######  Theorem 5 (Paring).

$(V,\in)$ has finite propositional tupling.

###### Proof.

Given a finite $A:\operatorname{Type}$ and $v:A\rightarrow V$ we let
$\\{v\\}:=\sup(\operatorname{image}v,\operatorname{incl}v)$, which then has
the desired property.∎

Taking the graph of a function and maping the von Neumann numerals into $V$
are already embeddings. Therefore, we need not take any images when
constructing these and the proofs are identical to the ones in “From multisets
to sets in HoTT”[8].

######  Theorem 6 (Exponentiation).

Any ordered pairing structure $\langle-,-\rangle$ on $V$ has exponentiation.

###### Proof.

Given any $a,b:V$, where $a\equiv\sup(A,g)$ and $b\equiv\sup(B,g)$, we let
$a\Rightarrow b:=\sup(A\rightarrow B,\lambda h\rightarrow\sup(A,\lambda
a\rightarrow\langle a,g\,(h\,a)\rangle$. This then has the required property.∎

######  Theorem 7 (Natural numbers).

$(V,\in)$ has an accessible natural numbers set.

##  4 Constructing the terminal $\operatorname{P}_{U}$-coalgebra

In this section we construct the terminal $\operatorname{P}_{U}$-coalgebra
from the M-type
$M_{\infty}:=\rotatebox[origin={c}]{-180.0}{$\operatorname{W}$}_{A:U}A$.
M-types were constructed in HoTT by Ahrens et al[4]. By inspecting their
constructions, one can see that $M_{\infty}$ is locally $U$-small – which is
important when we apply Assumption 1.

######  Definition 27.

The coiterative hierarchy of multisets is defined as
$M_{\infty}:=\rotatebox[origin={c}]{-180.0}{$\operatorname{W}$}_{A:U}A$. Its
deconstructor is denoted
$\operatorname{desup}_{\infty}:M_{\infty}\rightarrow\sum_{A:U}(A\rightarrow
M_{\infty})$ and is an equivalence. Furthermore, given any type $X$ and map
$m:X\rightarrow\sum_{A:U}(A\rightarrow X)$ the map denoted
$\operatorname{corec}_{\infty}m:X\rightarrow M_{\infty}$ is the one given by
the universal property of $M_{\infty}$ as an M-type.

The underlying type of the final $\operatorname{P}_{U}$-coalgebra,
$V_{\infty}^{0}$, is going to be the image of an endo-function
$\sigma:M_{\infty}\rightarrow M_{\infty}$. Thus, it can be seen as a kind of
quotient of $M_{\infty}$ where we have a canonical choice of elements in each
equivalence class.

######  Definition 28.

Let $\sigma:M_{\infty}\rightarrow M_{\infty}$ be defined by
$\sigma:\operatorname{corec}_{\infty}((\lambda(A,f).(\operatorname{image}\,f,\operatorname{incl}\,f))\circ\operatorname{desup}_{\infty})$.

The coiterative sets is then defined as the subtype of coiterative multisets
which are in the image of $\sigma$.

######  Definition 29.

$\displaystyle\operatorname{coiterative-
set}:M_{\infty}\rightarrow\operatorname{Type}$
$\displaystyle\operatorname{coiterative-set}\,a:=\exists_{b:M}\sigma\,b=a$

The universe of all coiterative sets is then the underlying type of our main
construction, the terminal $\operatorname{P}_{U}$-coalgebra.

######  Definition 30.

Let $V^{0}_{\infty}:=\sum_{a:M}\operatorname{coiterative-set}\,a$. Hence
$V^{0}_{\infty}$ is the image of $\sigma$.

######  Definition 31.

Let $\operatorname{coiterative-image}:M_{\infty}\twoheadrightarrow
V^{0}_{\infty}$ be the surjection given by $\operatorname{coiterative-
image}\,x:=(\sigma\,x,\left|\sigma\,x,\operatorname{refl}\right|)$.

The diagram in 4 summarises the construction of $V^{0}_{\infty}$: The top
square is the coalgebra homomorphism property of $\sigma$, given by its
corecursive definition. The bottom triangle is the image factorisation of
$\sigma$. We will not use this to prove that $V^{0}_{\infty}$ is a terminal
$\operatorname{P}_{U}$ coalgebra.

$\textstyle{\sum_{A:U}A\rightarrow
M_{\infty}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sum_{A}\sigma^{A}}$$\textstyle{\sum_{A:U}A\rightarrow
M_{\infty}}$$\textstyle{\sum_{A:U}A\rightarrow
M_{\infty}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(A,f)\mapsto(\operatorname{image}\,f,\operatorname{incl}\,f)}$$\textstyle{M_{\infty}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\operatorname{desup}_{\infty}}$$\scriptstyle{\sigma}$$\textstyle{M_{\infty}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\operatorname{desup}_{\infty}}$$\textstyle{V^{0}_{\infty}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$
Figure 4:  Diagram defining $V^{0}_{\infty}$ from the universal property of
$M_{\infty}$ as a terminal coalgebra and image factorisation.

The next two lemmas construct the coalgebra structure of $V^{0}_{\infty}$,
i.e. a map
$\operatorname{desup}^{0}_{\infty}:V^{0}_{\infty}\rightarrow(\sum_{A:U}A\rightarrow
V^{0}_{\infty})$.

######  Lemma 10 (Idempotency of $\sigma$).

Given $a:V^{n}_{\infty}$ then $\sigma(\pi_{0}\,a)=\pi_{0}\,a$.

###### Proof.

Immediate, since the underlying maps are already $-1$ truncated.∎

######  Lemma 11.

$\operatorname{desup}_{\infty}:M_{\infty}\rightarrow(\sum_{A:U}A\rightarrow
M_{\infty})$ restricts to an equivalence
$\operatorname{desup}^{0}_{\infty}:V^{0}_{\infty}\rightarrow(\sum_{A:U}A\hookrightarrow
V^{0}_{\infty})$. Its inverse will be denoted $\sup^{0}_{\infty}$.

###### Proof.

Since
$\operatorname{desup}_{\infty}:M_{\infty}\rightarrow\sum_{A:U}(A\rightarrow
M_{\infty})$ is an equivalence, it is sufficient to very that for every
$x:M_{\infty}$ that $x$ is an coiterative set if and only if
$(A,f)\equiv\operatorname{desup}_{\infty}\,x$ is such that $f:A\rightarrow M$
is an embedding and factors through $\pi_{0}:V^{0}_{\infty}\hookrightarrow M$.

Left-to-right

Assume that $x$ is in the image of $\sigma$. What we are to show is a
proposition, so we can assume that we are given $b:M$ such that $\sigma\,b=x$.
Let $(B,g)=\operatorname{desup}\,b$. The diagram in Figure 4 gives that that
there is $\alpha:A=\operatorname{image}g$ and
$f=\sigma\circ\operatorname{incl}\,g\circ\operatorname{coe}\,\alpha$. But
$\sigma=\pi_{0}\circ\operatorname{coiterative-image}$ and thus
$f=\pi_{0}\circ\operatorname{coiterative-
image}\circ\operatorname{incl}\,g\circ\operatorname{coe}\,\alpha$ is a
factorisation of $f$ through $\pi_{0}$.

Right-to-left

Assume that $f:A\hookrightarrow M_{\infty}$ and that $f=\pi_{0}\circ
f^{\prime}$, for some $f^{\prime}:A\hookrightarrow V^{0}_{\infty}$. In other
words have $\operatorname{desup}_{\infty}\,x=(A,\pi_{0}\circ f^{\prime})$. The
top square of Figure 4 gives
$\operatorname{desup}_{\infty}(\sigma\,x)=(\operatorname{image}\,f,\sigma\circ\operatorname{incl}\,(\pi_{0}\circ
f^{\prime}))$ which is just $(A,\sigma\circ\pi_{0}\circ f^{\prime})$, since
$\pi_{0}\circ f^{\prime}$ is already an embedding.

By Lemma 10,
$\operatorname{desup}_{\infty}(\sigma\,x)=(A,\sigma\circ\pi_{0}\circ
f^{\prime})=(A,\pi_{0}\circ f^{\prime})$, which is
$\operatorname{desup}_{\infty}x$. Since
$desup_{\infty}(\sigma\,x)=\operatorname{desup}_{\infty}x$ we can conclude
that $\sigma\,x=x$ and hence $x$ is in the image of $\sigma$, and an
coiterative set.

∎

######  Theorem 8 (The small powerset functor has a final coalgebra).

$(V^{0}_{\infty},\operatorname{desup}^{0}_{\infty})$ is a terminal
$\operatorname{P}_{U}$ coalgebra.

###### Proof.

Given a $\operatorname{P}_{U}$-coalgbra $(X,m)$, where $X:\operatorname{Type}$
and $m:X\rightarrow\operatorname{P}_{U}\,X$, we get the required homomorphism
map by first post-composing $m$ with the projection map
$\operatorname{P}_{U}\,X\rightarrow\sum_{A:U}A\rightarrow X$. That map yields
by $M_{\infty}$ corecursion a homomorphism into $M_{\infty}$, from which we
get back to $V^{0}_{\infty}$ using $\operatorname{coiterative-image}$.

(15)

The top map of the right square is
$(A,f)\rightarrow(\operatorname{image}\,f,\operatorname{coiterative-
image}\circ\operatorname{incl}\,f)$, and the square commutes by definition of
$\operatorname{coiterative-image}$ and $\sigma$.

Composing the squares we obtain the required coalgebra homomorphism. Then,
consider the following monomorphism diagram to see that the homomorphism is
unique:

(22)

If there was another choice of homomorphism $X\rightarrow V^{0}_{\infty}$, it
would induce a another homomorphism from $X$ to $M_{\infty}$. But because of
terminality of $M_{\infty}$ the two induced homormophisms would be the same,
and the map $V^{0}_{\infty}\hookrightarrow M$ is an embedding, the original
two homomorphisms $X\rightarrow V^{0}_{\infty}$ must also be the same.∎

##  5 Anti-Foundation in the terminal $\operatorname{P}_{U}$-coalgebra

In this section we show that given a terminal
$\operatorname{P}_{U}$-coalgebra, the $\in$-structure defined in 3 will
satisfy Anti-Foundation.

For sake of completeness and comparason, we first include a proof that if we
let $\in:M_{\infty}\rightarrow M_{\infty}\rightarrow\operatorname{Prop}$ be
defined by $x\in\sup_{\infty}(A,f):=\sum_{a:A}f\,a=x$, we get a
$\in$-structure satisfying the multiset anti-foundation:

######  Theorem 9 (Multiset anti-foundation).

The $\in$-structure $(M_{\infty},\in)$, with any ordered pairing structure,
satisfies multiset anti-foundation.

###### Proof.

Given a graph $g$ we have to construct a map $d:M\rightarrow M$, such that
$z\in d\,x\simeq\sum_{y:M}(\langle x,y\rangle\in g)\times(d\,y=z)$. We
construct this map by using $g$ to construct a new co-algebra structure on
$M$, namely:

$\displaystyle m_{g}:M\rightarrow\sum_{A:U}(A\rightarrow M)$ $\displaystyle
m_{g}\,x:=((\sum_{y:M}\langle x,y\rangle\in g),\pi_{0})$

(For convenience we coerce along the fact that $\sum_{y:M}\langle
x,y\rangle\in g$ is essentially $U$-small)

This induces, by terminality of $M$, a function $d:M\rightarrow M$ with the
property: if $d\,x\equiv\sup A\,f$ then $\alpha:\left(\sum_{y:M}\langle
x,y\rangle\in g\right)\simeq A$ and $f\,(\alpha(y,p))=d\,y$.

So, we compute

$\displaystyle z\in d\,x$ $\displaystyle\simeq\sum_{p:\sum_{y:M}\langle
x,y\rangle\in g}d(\pi_{0}\,p)=z$ $\displaystyle\simeq\sum_{y:M}(\langle
x,y\rangle\in g)\times d\,y=z$

as required. Uniqueness of $d$ is immediate from the terminality of $M$∎

The proof of anti-foundation for $V^{0}_{\infty}$ follows the same idea, that
a graph gives a new coalgebra structure on $V^{0}_{\infty}$, which induces the
needed endofunction $d$:

######  Theorem 10 (Anti-foundation).

The $\in$-structure $(V^{0}_{\infty},\in)$, with any ordered pairing
structure, satisfies anti-foundation.

###### Proof.

Given a graph $g$ we have to construct a map $d:V^{0}_{\infty}\rightarrow
V^{0}_{\infty}$, such that $z\in d\,x\simeq\exists_{y:M}(\langle x,y\rangle\in
g)\times(d\,y=z)$. The $V^{0}_{\infty}$-analogue of the coalgebra form the
proof of 9 will work:

$\displaystyle m_{g}:V^{0}_{\infty}\rightarrow\sum_{A:U}(A\hookrightarrow
V^{0}_{\infty})$ $\displaystyle m_{g}\,x:=((\sum_{y:V^{0}_{\infty}}\langle
x,y\rangle\in g),\pi_{0})$

Note that $\pi$0 is indeed an embedding since $\langle x,y\rangle\in g$ is a
mere proposition.

Because of terminality of $V^{0}_{\infty}$ we get an induced map
$d:V^{0}_{\infty}\rightarrow V^{0}_{\infty}$ with the property that for
$\operatorname{desup}_{\infty}\,(d\,x)=(\operatorname{image}(d\circ\pi_{0}),\operatorname{incl}(d\circ\pi_{0}))$
where $\pi_{0}:\left(\sum_{y:V^{0}_{\infty}}\langle x,y\rangle\in
g\right)\rightarrow V^{0}_{\infty}$. Or, diagramatically, spelling out the
image of $d\circ\pi_{0}$ as the sum of mere fibres, there must exist an
$\alpha$ which makes the diagram commute:

We therefore can compute:

$\displaystyle z\in d\,x$
$\displaystyle\equiv\sum_{a:\operatorname{image}(d\circ\pi_{0})}\operatorname{incl}(d\circ\pi_{0})\,a=z$
(23)
$\displaystyle\simeq\sum_{q:\sum_{z:V^{0}_{\infty}}\exists_{y:V^{0}_{\infty}}(\langle
x,y\rangle\in g)\times d\,y=z}\pi_{0}\,q=z$ (24)
$\displaystyle\simeq\exists_{y:V^{0}_{\infty}}(\langle x,y\rangle\in g)\times
d\,y=z$ (25)

which is what we needed. Uniqueness is immediate from the terminality of
$V^{0}_{\infty}$.∎

We end this section with a few exampeles of non-wellfounded sets constructed
in the model.

######  Example 2 (Quine atom).

A Quine atom is a set $x$ with the property that $x=\\{x\\}$. The essence of
the Quine atom can be found in the coalgebra
$m:1\rightarrow\left(\sum_{A:U}A\rightarrow 1\right)$, given by
$m\,x:=(1,\lambda x.*)$. This coalgebra induces a map $q:1\rightarrow
M_{\infty}$, such that $\operatorname{desup}(q\,*)=(1,\lambda x.q\,*)$. We
compute: $z\in(q\,*)=\sum_{x:1}(z=q\,*)=(z=q\,*)$, which is exactly what it
means for $q\,*$ to be a quine atom.

######  Example 3 (Conatural numbers).

Another frequent example of a non-wellfounded set is the conoatural numbers.
In type theory one can see conatural numbers as an M-type,
$\rotatebox[origin={c}]{-180.0}{$\operatorname{W}$}_{x:1+1}x=\operatorname{left}*$,
or as the terminal coalgebra for the polynomial $\lambda X.1+X$, or the type
of increasing binary sequences (For a specific construction, see Escardo’s
Agda-formalisation[6]).

In our model we can use the terminal-coalgebra-for-$(\lambda X.1+X)$
formulation, to construct the the coiterative set of conaturals. Let
$\mathbb{N}_{\infty}$ be the type of conaturals its coalgebra structure
$n:\mathbb{N}_{\infty}\rightarrow\mathbb{N}_{\infty}+1$. We can construct a
map
$q:\mathbb{N}_{\infty}+1\rightarrow\operatorname{P}_{U}\,(\mathbb{N}_{\infty})$
by $q(\operatorname{left}\,x)=(1,\lambda i.x)$ and
$q(\operatorname{right}\,x)=(0,e)$ (where $e$ is the empty function). Thus we
get a $\operatorname{P}_{U}$-coalgebra structure on $\mathbb{N}_{\infty}$.
This gives a map $r:\mathbb{N}_{\infty}\rightarrow V^{0}_{\infty}$, which can
be shown to be injective, and the conatural numbers internal to
$V^{0}_{\infty}$ can thus be given as
$\sup_{\infty}^{0}(\mathbb{N}_{\infty},r)$.

##  6 Conclusion

We have found a model – in homotopy type theory – of constructive set theory
with Aczel’s anti-foundation axiom. For the sake of reference, here is main
theorem summarising the results in the previous two sections:

######  Theorem 11 (The Coiterative Hierarchy).

There is a $\in$-strucure $(V_{\infty}^{0},\in)$ satisfying the following
axioms, when all quantifiers are interpreted as truncated, and equality is the
identity type:

  * •

Extensionality

  * •

Pairing

  * •

Replacement

  * •

Union

  * •

Restricted separation

  * •

Exponentiation

  * •

Empty set

  * •

Natural numbers

  * •

Aczel’s Anti-Foundation Axiom

One remaining question is if it is possible to do without Assumption 1.
Perhaps it could be replaced by mere set quotients, since the resulting model
is a mere set. But on the other hand the assumption is interesting in itself,
and could warrant further investigation as a constructive principle.

## References

  * [1] Peter Aczel.  The type theoretic interpretation of constructive set theory.  In A. MacIntyre, L. Pacholski, and J. Paris, editors, Logic Colloquium ’77, pages 55–66. North–Holland, Amsterdam-New York, 1978.
  * [2] Peter Aczel.  Non-well-founded sets, volume 14 of CSLI Lecture Notes.  Stanford University, Center for the Study of Language and Information, Stanford, CA, 1988.  With a foreword by Jon Barwise [K. Jon Barwise].
  * [3] Peter Aczel and Michael Rathjen.  Notes on constructive set theory.  Technical report, Institut Mittag-Leffler, 2001.
  * [4] Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti.  Non-wellfounded trees in homotopy type theory.  In 13th International Conference on Typed Lambda Calculi and Applications, volume 38 of LIPIcs. Leibniz Int. Proc. Inform., pages 17–30. Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2015\.
  * [5] Giovanna D’Agostino and Albert Visser.  Finality regained: a coalgebraic study of Scott-sets and multisets.  Arch. Math. Logic, 41(3):267–298, 2002.  doi:10.1007/s001530100110.
  * [6] Martin Escardo.  Co-natural numbers in agda.  URL: https://www.cs.bham.ac.uk/~mhe/agda-new/CoNaturals.html.
  * [7] Marco Forti and Furio Honsell.  Set theory with free construction principles.  Ann. Scuola Norm. Sup. Pisa Cl. Sci. (4), 10(3):493–522, 1983.  URL: http://www.numdam.org/item?id=ASNSP_1983_4_10_3_493_0.
  * [8] Håkon Robbestad Gylterud.  From multisets to sets in homotopy type theory.  The Journal of Symbolic Logic, 83(3):1132$\textendash$1146, 2018.  doi:10.1017/jsl.2017.84.
  * [9] Håkon Robbestad Gylterud.  Multisets in type theory.  Mathematical Proceedings of the Cambridge Philosophical Society, page 1$\textendash$18, 2019.  doi:10.1017/S0305004119000045.
  * [10] Ingrid Lindström.  A construction of non-well-founded sets within Martin-Löf’s type theory.  J. Symbolic Logic, 54(1):57–64, 1989.  doi:10.2307/2275015.
  * [11] The Univalent Foundations Program.  Homotopy Type Theory: Univalent Foundations of Mathematics.  homotopytypetheory.org, Institute for Advanced Study, 2013.  URL: http://homotopytypetheory.org/book.
  * [12] Benno [van den Berg] and Federico [De Marchi].  Non-well-founded trees in categories.  Annals of Pure and Applied Logic, 146(1):40 – 59, 2007.  URL: http://www.sciencedirect.com/science/article/pii/S0168007207000024, doi:https://doi.org/10.1016/j.apal.2006.12.001.