{'fraction_non_alphanumeric': 0.05851602706974105, 'fraction_numerical': 0.0057948697167402845, 'mean_word_length': 3.6439593526533685, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 8, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Non-wellfounded sets in homotopy type theory

We construct a model of constructive set theory with Aczel's anti-foundation axiom (AFA) in homotopy type theory. Like the previous such model (Lindstr\"om 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 sits at the bottom of a hiearchy of non-wellfounded \in-structures of each h-level, and establish a duality with a hiearchy of well-founded \in-structures -- and in particular the model of set theory constructed in the book Homotopy Type Theory.


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 [6]. 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. 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 below 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 → 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 ∈-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 equalitycalled the identity type. Using the univalence axiom, we can compute the identity type for Aczel's model. In [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 coinductively what it means for an element of the M-type, W A:U A, of coiterative types, to be a coiterative set. The solution found uses the ability to form images of functions, and the universal property of M -types. For an introduction to M-types, and a proof of their existence in homotopy type theory, see [3].
While our target is a model of set theory where the identity type and ∈-relation are both mere propositions, we will indulge in a bit of generalisation. We will construct two hierarchies of models V n and V n ∞ for n : N. The model V 0 is equivalent to the one constructed in chapter ten of Homotopy Type Theory [11] and [8], while V 0 ∞ is the model of anti-foundation we are searching for. These models will be what we call ∈-structures, a generalisation of model of set theory to higher homotopy levels. The upper index on V n and V n ∞ denote their h-level, and by extensionality both the identity type and the ∈-relation will be of level n − 1. Thus, V 0 and V 0 ∞ are mere sets with x = y and x ∈ y being mere propositions.
At the next level, V 1 and V 1 ∞ , the types x ∈ y will be mere sets. The elements of this type can be though of as occurrences of x in y -in the sense that y is a multiset. For instance, the type ∅ ∈ [∅, ∅] would have two distinct elements. This view of multisets is further elaborated in [9].
A hierarchy of wellfounded models, similar to our V n , was studied by Gallozzi [7]. The relationship to our hierarchy can be summarised as follows: Instead of restricting elements of V n to n − 1-truncated functions A → V n , Gallozzi restricts the domain A to n-types.
The relationship between multisets and non-wellfounded sets was also studied in [4], but from a classical point of view with a ternary predicate x ∈ κ y meaning x occurs in y κ-many times, for a cardinal κ.

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 : Type -we take Type to be a univalent universe of large types.
• f a denotes the application of the function f to the element a.
• U is a univalent universe (of small types). We suppress the notation of the decoding family, such that A : U will entail A : Type. • W a:A B a denotes the W-type inductively generated by sup : a: a:A B a denotes the M-type defined coinductively by desup : W a:A B a → a:A (A → W a:A B a). We use a rotated W, instead of M to distinguish it from the structures denoted M .
• Fin n denotes a specific choice of finite types, where Fin n has n elements. • π 0 : ( a:A B a) → A is the first projection. A notable special case is when B a is a proposition for all a, then π 0 is an embedding. • π 1 : ( a:A B a) → B (π 0 a) is the second projection.
• A ֒→ n B denotes the type of n − 1-truncated 1 functions (See 7.6 of [11] for definition of n-truncated functions) from A to B. If the index is omitted it is assumed to be 0, so that A ֒→ B takes its usual meaning as the type of embeddings of A into B.

Images of small types
When constructing the models, one operation will be of special interest, namely taking the image of a map. If the map f : A → B is between two types in our given universe, the resulting image, given as the type b:B a:A f a = b −1 , also lies in the universe -as long as the universe is closed under propositional truncation. But if only the domain, not the codomain, lies in U , it is not obvious that the image of the function would lie in U . We will now defined an extended replacement principle for universes, which says that images of small types into locally small types are small.
Lemma 1. Being essentially U -small is a mere proposition.
Proof. We must show that the type A:U A ≃ X is a mere proposition. This type looks close to being of the form 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, α) and (B, β) be two elements of A:U A ≃ X. Applying univalence, we observe that It remains to show that we get β by transporting α along the path ua(β −1 · α), in the family λ(Y : U ).Y ≃ X. But this is easily computed with path algebra: Definition 3. A univalent universe, U , is said to be image complete if for every locally U -small type X and every A : U and f : A → X, the image of f is essentially U -small.
Not every univalent universe is image complete. For instance, given any univalent universe U , we can define the subuniverse of mere sets, Set U , which is not image complete because the map (λx.2) : 1 → U which maps the point to the booleans in the universe has an image which is not a set: there is a non-trivial equality 2 = 2 in the universe arising from univalence and the negation equivalence 2 ≃ 2 which would lie in the image. Definition 4. A univalent universe, U , is said to be n-image complete if for every locally U -small type X and every A : U and f : A → X, the n-image of f is essentially U -small.
From this point on, we will assume that our universe, U , is n-image complete. For every n ≥ 0 and locally U -small type X, we will denote by ι X,n : ( A:U A → X) → ( A:U A → X) the map which assigns to each pair (A, f ) a representation of its n − 1-image in U and the induced inclusion into X.
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 ∈-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 ∈-structures in these terms.
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 interesting 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 ∈-structure such an ordered paring-structure.
Here, we are also making a generalisation. Because we are working in homotopy type theory, we do not have to require that the underlying type of sets is a mere set, nor do we have to require that x ∈ y is a mere proposition. As observed in [9], we can consider the general case where these are types of any kind. With care, we can still state the usual properties we know and love from set-theory, and prove that they hold.
The usual notion of (extensional) model of set theory corresponds to ∈-structures, (M, ∈), where x ∈ y is a mere proposition for each x, y : M (and consequently M is a mere set). However, there are examples of extensional ∈-structures where M is not a mere set. In the next section we will construct two hierarchies of ∈-structures, where only the lowest model in each hierarchy has a propositional ∈-relation.

Properties for ∈-structures
Now we will look at generalisations of some of the usual notions from set theory to ∈-structures. Most of these are properties which are mere propositions, which an ∈-structure can satisfy in at most one way. Other notions, such as ordered tupling, are structures which have to be specified.
Restricted separation, pairing, singletons, union-replacement, infinity and exponentiation/fullness were defined in [9]. The concept of U -likeness was originally stated for propositional ∈-structures in [8] mimicking the notion of set-likeness from classical set theory.
One general observation is that any elements, say u : M , defined by a type P such that z:M z ∈ u ≃ P are uniquely defined (if they exist). Thus, most of the axioms are mere propositions. An exception to this rule is the axiom of infinity: In INF, u occurs in its defining formula, thus to prove that u unique, we would have to apply ∈-induction, which does not hold in all ∈-structures. In fact, in the non-wellfounded models we will construct in the next section there will be two different terms proving INF -one for the natural numbers, and one for the co-natural numbers.

Forming finite sets
In usual set theory the axiom of pairing let us form sets from finite lists {x 0 , · · · x n−1 } from the empty set by iteration: {x 0 , · · · , x n } = ∪{{x 0 , · · · x n−1 }, {x 0 , x 0 }}. We will instead form n-tuples directly: Definition 6. An ∈-structure, (M, ∈), has finite tupling if for every finite type A and every vector v : A → M there is {v} : M such that for every z : M we have z ∈ {v} ≃ ∃ a:A v a = z.
Since tupling is a proposition, for any given ∈-structure it is sufficient to prove the existence of {v} for every v : Fin n → M to show that it has tupling.
The definition of finite tupling uses the truncated existential quantifier. It is natural to also consider the case where we use the normal, everyday Σ-type.

Ordered pairing
While unordered tuples are defined up to equality in a ∈-structure, the ordered tuples are not. Indeed usual set theory provides us with many different ways of constructing ordered pairs. Because of this, we will assume unordered pairing as an extra structure.  Proof. We must show that for every x : M we that a,b:M a, b = x is a mere proposition. Let ((a, b), α) and ((a ′ , b ′ ), β) be two of its elements. Clearly β −1 ·α : a, b = a ′ , b ′ , hence (a, b) = (a ′ , b ′ ). Transporting α along this equality we obtain β by the usual transport gymnastics. Thus we have that ((a, b), α) = ((a ′ , b ′ ), β).

U-likeness
In this subsection we review the relationship between ∈-structures and coalgebras for the polynomial functor A:U A → X. Furthermore, we see that models of propositional set theory are exactly coalgebras M ֒→ A:U A ֒→ M . Definition 9. Given an ∈-structure, (M, ∈), we define the family E : M → Type by E a = x:M x ∈ a.
Definition 10. An ∈-structure, (M, ∈) is U -like if E a is essentially U -small for every a : M . To simplify notation, we will coerce E a : U in U -like ∈-structures.
The equivalence (4)  The follow theorem combines the two previous lemmas in order to characterise ∈-structures of various h-levels in terms of coalgebras. Proof. Simple corollary of the previous two lemmas.

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 ∈-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 14. Given an ∈-structure, (M, ∈), with an ordered paring structure, −, − : M → M → M , we say that a element g : M is a graph if every element of g is a pair -that is e:g e ∈ g → a,b:M e = a, b .
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 ∈-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 g = { x, y , x, z } and an assignment d if we want the type (d y ∈ d x) to have one or two elements. At first it might seem like the reasonable answer is one since x, y ∈ 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 x, y and x, z . So, two coherent answers to this question are that either we count the edges to each bisimilar node or we truncate to make ∈ a propositional relation. 2 Definition 18. Given an ∈-structure, (M, ∈), with an ordered paring structure, −, − , we say that it satisfies mere anti-foundation if every graph, g, has a unique mere decoration. That is, the type d:M→M x,z:M (z ∈ d x ≃ ∃ y:M ( x, y ∈ g) × (d y = z)) is contractible.

The model
We will now develop -in parallel -the two dual models of set theory. The first is the inductive model described in [8] and the dual is a new model, satisfying the anti-foundation axiom. These will be found at the bottom of a hierachy of ∈-structures, based on the W-and M-types previously used by Aczel [1] and Lindström [10] in their setoid based models of constructive set theory. First we define the base types 3 M := W A:U A and M ∞ := W A:U A, from which we will carve a hierarchy of ∈-substructures. We will slightly abuse notation and denote by "sup" both sup : A:U A → M and sup : A:U A → M ∞ . In each case sup is an equivalence and we denote the inverses (with equal amounts of syntactic abuse) by desup. And, we define x ∈ (sup A f ) := i:A f i = x.
These two types, M and M ∞ , are the initial and terminal U -like ∈-structures. This is clear in light of Lemma 3, which elaborates the connection between U -like ∈-structures and coalgebras.
Remember that for n ≥ 0 we have a transformation ι X,n : ( A:U A → X) → ( A:U A → X). By pre-and post-composition with this transformation, we can define new algebra and co-algebra structures on M and M ∞ -these will because of initiality/finalness have induced maps to our original structures. We call these maps ρ n : M → M and σ n : M ∞ → M ∞ -they are uniquely defined by the commuting squares in Figure 4 and 5. These squares will be our main tools in the proofs below.

Definition 19.
iterative-n-type : M → Type iterative-n-type a := ∃ b:M ρ n b = a Definition 20. We define V n := a:M iterative-n-type a -the image of ρ n . See also Figure 4.
We denote by (V n , ∈ n ) the induced sub-∈-structure of M .
coiterative-n-type : M ∞ → Type coiterative-n-type a := ∃ b:M σ n b = a Definition 22. We define V n ∞ := a:M coiterative-n-type a -the image of σ n . See also Figure 5. We denote by (V n ∞ , ∈ n ∞ ) the induced sub-∈-structure of M ∞ .
Example 1 (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 → ( A:U A → 1), given by m x := (1, λx. * ). This coalgebra induces a map q : 1 → M ∞ , such that desup(q * ) = (1, λx.q * ). We compute: z ∈ (q * ) = x:1 (z = q * ) = (z = q * ), which is exactly what it means for q * to be a quine atom. 3 The "∞"-subscript is used here to indicate the analogy with the usual notation for co-natural numbers N∞. Figure 4: Diagram defining V n from the universal property of M as an initial algebra and image factorisation.
Example 2 (Conatural numbers). We briefly mentioned that the usual defining property for the natural numbers: z:M z ∈ u ≃ Z z + y:M y ∈ u × S y z , actually does not define u up to equality in M ∞ . On the one hand we have the usual natural numbers in M , originally defined by Aczel [1]. On the other hand, we have the co-natural numbers, N ∞ : U , as defined for instance in [5], the terminal coalgebra for the polynomial λX.1 + X. We can define another coalgebra structure m : N ∞ → A:U A → N ∞ by m k = ( l:N∞ l ≺ k, π 0 ), where ≺ is the relation x ≺ succ n x for some n > 0. Then the element m ω will then also have the required property.
Proof. Immediate, since the underlying maps are already n − 1 truncated.
Proof. Immediate, since the underlying maps are already n − 1 truncated.  Figure 4 we have: Hence, sup A f is in the image of ρ n and thus an iterative n-type. Right-to-left: What we are to show is a proposition, so we can assume that we are given b : M such that ρ n b = sup A f . Assuming b ≡ sup Bg, we know by definition of ι n , and the diagram in Figure 4 that ρ n • g = f • h for some n-connected h : B → A, and that f is n-truncated. Since the n-factorisation of ρ n • g, namely f • h, factors through its −1-factorisation, we get an induced map f ′ : . We denotes its inverse by sup n ∞ . The rest of the proof is dual to the previous.
Proof. Dually to the previous lemma, it is sufficient to very that for every x : M ∞ that x is an iterative n-type if and only if (A, f ) ≡ desup x is such that f : A → M is n-truncated and factors through π 0 : V n ∞ ֒→ M .

Lemma 10.
For all x, y : V n the type x ∈ n y is an n − 1-type.
Proof. Since sup n is an equivalence, we can assume that y ≡ sup n A f for A : U and f : Lemma 11. For all x, y : V n ∞ the type x ∈ n ∞ y is an n − 1-type.
Proof. Since sup n is an equivalence, we can assume that y ≡ sup n ∞ A f for A : U and f : Lemma 12. V n and V n ∞ are transitive sub-∈-structures of M and M ∞ , respectively.
Proof. We must show that given x ∈ y in M , if y is an iterative n-type, then so is x. Since sup n is an equivalence we can assume y ≡ sup n Af . Since x ∈ y there is a : A such that π 0 (f a) = x, Thus, by Lemma 6, we have ρ n x = ρ n (π 0 (f a)) = π 0 (f a) = x, hence x is an iterative n-type. The same proof goes for the V ∞ case, using Lemma 7 instead.
Lemma 13. V n and V n ∞ are n-types.
Proof. This is immediate from extensionality, a = b ≃ c (c ∈ a) ≃ (c ∈ b), and the fact that c ∈ a and c ∈ b are n − 1 types.
Another easy exercise, left to the reader, is to show that the well-founded parts of M ∞ and V n ∞ are M and V n , respectively: Lemma 14. W F M∞,∈ = (M, ∈) and for all n ≥ 0 we have W F V n ∞ ,∈ n ∞ = (V n , ∈ n ) Theorem 2. (V n , sup n ) is the initial "power-n-type" algebra and (V n ∞ , desup n ∞ ) is the terminal "power-ntype" coalgebra -where the power-n-type operation maps a locally U -small type X to the type A:U A ֒→ n X.
Proof. Initiality: Given an algebra m : ( A:U A ֒→ n X) → X, we can precompose with ι X,n to get an algebra for ( A:U A → X) -regarding A:U A ֒→ n X as the image of ι X,n . This induces a unique homomorphism from (M, sup), which we can precompose with the inclusion V n ֒→ M , which yields a the required commutative square: Uniqueness similarly follows from uniqueness of the homomorphism M → X, since we can use the composition above to obtain an alternative map M → X by factoring through the surjection M → V n : If there was another choice of homomorphism V n → X, it would induce a another homomorphism from M to X. But because of initiality of M the two induced homormophisms would be the same, and the map M ։ X is an epimorphism, the original two homomorphisms V n → X would also be the same.
Terminality: Exactly dually, we compose the following two squares to get the homomorphism: And consider the following monomorphism diagram to see that the homomorphism is unique: By looking at the proofs in [8], we see that in order to prove replacement, union, pairing, restricted separation and exponentiation for V 0 , we only use the fact that V 0 is a fixed point for the operation λX. A:U A ֒→ X. Thus, we do not have to repeat the proofs for V 0 ∞ , since it is also a fixed point of this operation. Thus we go straight to showing that the anti-foundation properties hold. Proof. Given a graph g we have to construct a map d : M → M , such that z ∈ d x ≃ y:M ( x, y ∈ g) × (d y = z). We construct this map by using g to construct a new co-algebra structure on M , namely:

Conclusion
We have found a model -in homotopy type theory -of constructive set theory with Aczel's anti-foundation axiom. Further more, we have shown that the merely propositional models of set theory are at the bottom of a larger hierarchy of iterative n-types, which seem like a promising concept for further study. It also remains to formalise the above results in a proof assistant, such as Agda. Such a formalisation could build on the existing formalisation of M-types in Agda [3], and the formalisation of the model of well-founded sets developed in [8].