{'fraction_non_alphanumeric': 0.059226003580366095, 'fraction_numerical': 0.008754088834319027, 'mean_word_length': 3.8365367180417045, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 30, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Comparing material and structural set theories

We study elementary theories of well-pointed toposes and pretoposes, regarded as category-theoretic or"structural"set theories in the spirit of Lawvere's"Elementary Theory of the Category of Sets". We consider weak intuitionistic and predicative theories of pretoposes, and we also propose category-theoretic versions of stronger axioms such as unbounded separation, replacement, and collection. Finally, we compare all of these theories formally to traditional membership-based or"material"set theories, using a version of the classical construction based on internal well-founded relations.

1. Introduction 1.1. Overview. It is well-known that elementary topos theory is equiconsistent with a weak form of set theory. The most common statement of this relates the theory of a well-pointed topos with a natural numbers object and satisfying the axiom of choice (a.k.a. ETCS; see [Law64]) to "bounded Zermelo" set theory (BZC). This is originally due to Cole [Col73] and Mitchell [Mit72]; see also Osius [Osi74] and for a more recent exposition [MLM94,Ch. VI]. Moreover, the proof is very direct: The author was supported by a National Science Foundation postdoctoral fellowship while writing the original version of this paper. While revising it he was supported by the United States Air Force Research Laboratory under agreement number FA9550-15-1-0053. The U.S. Government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon. The views and conclusions contained herein are those of the author and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of the United States Air Force Research Laboratory, the U.S. Government, or Carnegie Mellon University. the category of sets in any model of BZC is a model of ETCS, while from any model of ETCS one can construct a model of BZC out of well-founded relations. 1 Our goal is to obtain analogous results for stronger and weaker theories in a unified framework. On the one hand, by removing axioms such as choice, classical logic, and power sets from BZC, we obtain intuitionistic and predicative set theories which correspond to more general toposes and pretoposes. On the other hand, we propose category-theoretic properties which correspond to set-theoretic axioms such as separation, replacement, and collection. In particular, we characterize toposes that are the category of sets in a model of ZFC, as did Osius, Lawvere, and also McLarty [McL04]; but our result generalizes to the intutionistic case.
In this paper we deal entirely with (pre)toposes which correspond directly to set theories, in such a way that the set-theoretic elements of a set X are in bijection with its category-theoretic "global elements" 1 → X. In particular, any object of such a category must be determined by its global elements, which is to say that the terminal object 1 is a generator; that is, the category is well-pointed. (We will work with a constructive version of well-pointedness appropriate to intuitionistic logic. ) Of course, there is a further aspect to the classical story: if we drop wellpointedness, we can interpret BZC in any Boolean topos with an nno and choice by using the internal logic. In [Shu18], we will extend the usual internal logic to an interpretation we call the stack semantics that contains unbounded quantifiers, enabling all the results of this paper to be carried out "internally" in nonwell-pointed categories. Other related ways to deal with unbounded quantifiers include [JM95,ABSS14].
1.2. Some remarks on terminology. While "set theory" often refers only to membership-based theories such as ZFC and BZC, clearly ETCS and its ilk are also "theories about sets", and Lawvere has observed that ETCS can serve just as well as BZC as a foundation for much mathematics. Pursuant to this philosophy, we will use the term material set theory for theories based on a global membership predicate, such as BZC and ZFC, and structural set theory for theories which take functions as fundamental, such as ETCS.
In material set theories, the elements of a set X have an independent identity, apart from being collected together as the elements of X. Frequently, they are also sets themselves. The adjective "material" is a suggestion of Steve Awodey [Awo96]; these are also called "membership-based" set theories.
In structural set theories, the elements of a set X have no identity independent of X, and in particular are not sets themselves; they are merely abstract "elements" with which we build mathematical structures. Moreover, at least in the structural set theories we describe here, it is not meaningful to ask whether two elements of two different sets are equal; only whether two elements of a given ambient set are equal. Structural set theories are sometimes called "categorical" 2 set theories; we call them "structural" because they are closely aligned with the mathematical philosophy of "structuralism" (see e.g. [McL93,Awo04]), and because although they are usually formulated in the language of category theory, there is nothing intrinsically necessary about that (see e.g. [S + 09]).
As foundations for mathematics, material and structural set theory each have advantages and niches. Material set theory is well-adapted to the study of transfinite recursion and related subjects in pure set theory. However, structural set theory is arguably closer to mathematical practice outside of set theory, where the intricate ∈-structure of material set theory is irrelevant and objects need only be defined up to isomorphism. 3 Structural set theory is also more closely related to type theory, and might be considered a halfway-point between a material set-theoretic foundation and a type-theoretic one. The value of equivalences such as those we study here, then, is that they enable us to use whichever foundation is most appropriate for a given subject, with a canonical way to pass back and forth as necessary.
1.3. Summary of contents. We begin in §2 by listing some common axioms of material set theory, most of which should be familiar. Then in § §3-7 we develop general aspects of structural set theory. Little of this appears in the literature; the only papers we are aware of specifically about structural set theory are Lawvere's original [Law05] about ETCS, and the more recent [Pal09] which presents a predicative version thereof ("CETCS"), plus expository works such as [LR03,Lei14]. Our treatment is also a little idiosyncratic, due to a desire to remain isomorphisminvariant.
We begin in §3 by setting out the formal language we will use for category theory and recalling the basic notion of a Heyting pretopos, which underlies all our structural set theories. In §4 we add the further axiom of well-pointedness, which makes a Heyting pretopos into a structural set theory. Since well-pointedness has mostly been studied in a classical setting, we spend some time on the appropriate version thereof for a constructive theory, and its consequences. Then in §5 we rephrase the notion of "constructively well-pointed Heyting pretopos" in a way which looks more like a set theory.
In §6 we consider three further fairly straightforward axioms-full separation, fullness, and full induction-while in §7 we study collection and replacement axioms, which are rather more subtle. Replacement-type axioms for ETCS have been proposed by Lawvere [Law64], Cole [Col73], Osius [Osi74], and McLarty [McL04], but none of these is really suitable intuitionistically. We begin with collection, which relaxes the hypothesis of replacement by not requiring uniqueness. This is well-known to be important in weaker set theories, and its structural version is also easier to state. The structural replacement axiom is surprisingly subtle, since uniqueness is asserted only up to unique canonical isomorphism; we give a precise formulation of this and show that it follows from collection.
As we introduce each axiom of structural set theory, we prove that if V is a model of material set theory satisfying the corresponding material axiom, then the structural axiom is satisfied by its category of sets Set(V). Not until §8 do we turn to the reverse construction, originally due to Cole, Mitchell, and Osius, which produces a model V(Set) of material set theory starting from a suitable pretopos Set. As expected, we then show that if Set satisfies any given structural axiom, V(Set) satisfies the corresponding material axiom. In particular, we conclude that the following pairs of theories are equiconsistent: • Lawvere's ETCS and BZC, as in the classical theorems.
3 Indeed, Bourbaki, who enshrined a structuralist philosophy in their "general theory of structure" [Bou68], had to carefully specify exactly how the superfluous data of material set theory was to be forgotten, in order that all of their structures would be invariant under isomorphism.
• ETCS plus our axioms of collection or replacement (which are equivalent over ETCS and imply separation), and classical ZFC. • "Intuitionistic ETCS" (the theory of a constructively well-pointed topos with a nno), and "Intuitionistic BZ" (containing power sets and infinity). • Intuitionistic ETCS plus our axioms of separation and collection, and IZF.
• The theory of a constructively well-pointed Π-pretopos with a nno satisfiying our axioms of fullness, collection, and extensional well-founded induction, and Aczel's CZF augmented by Mostowski's principle. Finally, in §9 we consider the extent to which V(−) and Set(−) are inverses. This depends on foundation-type axioms in material set theory, and on a dual class of axioms for structural set theory that we call "materialization".
1.4. Conventions and Notation. We treat both material and structural set theories as theories in intuitionistic first-order logic (with a twist in the structural case; see §3). We regard classical logic as an axiom schema, ϕ ∨ ¬ϕ for all (or some) formulas ϕ, which may or may not be assumed in a theory or satisfied by a model.
All axioms and formulas are of course properly expressed in a formal first-order language. However, to make the paper easier to read for non-logicians, we will usually write such formulas out in English, trusting the reader to translate them into formal symbols as necessary. To make it clear when our mathematical English is to be interpreted as code for a logical formula, we will often use sans serif font and corner quotes. Thus, for example, in a structural set theory, every surjection has a section represents the axiom of choice.
1.5. Acknowledgements. I would like to thank Steve Awodey, Toby Bartels, Peter Lumsdaine, Colin McLarty, Thomas Streicher, Paul Taylor, and the patrons of the n-Category Café for many helpful conversations and useful comments on early drafts of this paper. The referee of the preliminary version also gave many helpful suggestions.

Material set theories
Our material set theories will be theories in one-sorted first order logic, with a single binary relation symbol ∈, whose variables are called sets. (We will briefly mention the possibility of "atoms" which are not sets at the end of this section.) Notation 2.1. There are two common conventions regarding the treatment of free variables in logical formulas. According to one convention, we should write ϕ(x 1 , . . . , x n ) to indicate that all the free variables of ϕ are among x 1 , . . . , x n , and then write ϕ(a 1 , . . . , a n ) for the result of substituting each a i for the corresponding x i . According to the other convention, in the first case we write ϕ without notating the free variables, and then ϕ[a 1 /x 1 , . . . , a n /x n ] for the result of substitution.
The former convention has the advantage of an easy and intuitive notation for substitution, plus explicit indication of the free variables. The latter convention is cleaner if there are many free variables but only a few are being substituted for.
In this paper we choose a middle ground. By a context we mean a finite list Γ = (x 1 , . . . , x n ) of distinct variables. (This definition will change slightly in the next section, where we use a typed logic.) A formula ϕ, written with no variables indicated, is said to be in context Γ if all of its free variables are found in Γ. However, we say a formula written as ϕ(x, y) (for instance) is in context Γ if all of its free variables other than x and y are found in Γ (and x and y do not appear in Γ). This convention allows us to carry around many free variables with unchanging values without needing to notate them constantly, yet retains a convenient notation indicating those free variables whose values do change.
In particular, this convention simplifies the statements of many of the axioms below. In all axiom schemas which are parametrized over a formula ϕ, ϕ(x), or ϕ(x, y), we assume this formula to exist in an ambient context Γ, whose variables are implicitly universally quantified outside each instance of the schema.
The prefix "∆ 0 -" on any axiom schema indicates that the formulas appearing in it are restricted to be ∆ 0 ; we sometimes use the adjective "full" to indicate the lack of any such restriction.
The following set of axioms (in intuitionistic logic) we call the core axioms; they form a subsystem of basically all material set theories.
• Extensionality: for any x and y, x = y if and only if for all z, z ∈ x iff z ∈ y . • Empty set: the set ∅ = {} exists .
• Pairing: for any x and y, the set {x, y} exists . • Union: for any x, the set { z | (∃y ∈ x)(z ∈ y) } exists .
• Limited ∆ 0 -replacement : For any ∆ 0 -formula ϕ(x, y), for all a and b, if for every x ∈ a there exists a unique y with ϕ(x, y), and moreover z ⊆ b for all z ∈ y, then the set { y | (∃x ∈ a)ϕ(x, y) } exists . The first five of these are standard, while the last, though very weak, is unusual. We include it because we want our core axioms to imply a well-behaved category of sets, for which purpose the other five are not quite enough. This axiom is satisfied in basically all material set theories, since it is implied both by ordinary replacement (even ∆ 0 -replacement), and by the existence of power sets (using ∆ 0 -separation).
We now list some additional common and important axioms of material set theory, pointing out the most important implications between them.
One major axis along which set theories vary is "impredicativity," expressed by the following sequence of axioms (of increasing strength): • Exponentiation: for any a and b, the set b a of all functions from a to b exists . • Fullness: for any a, b there exists a set m of entire relations from a to b such that for any entire relation f from a to b, there is a g ∈ m with g ⊆ f .
4 It is straightforward to prove that this Kuratowski definition of ordered pairs still has the correct behavior intuitionistically; see for instance [AR01].
• Power set: for any set x, the set P x = { y | y ⊆ x } exists .
Each of these is strictly stronger than the preceding one, but in the presence of either of the following: • ∆ 0 -classical logic: for any ∆ 0 -formula ϕ, we have ϕ ∨ ¬ϕ.
the hierarchy of predicativity collapses, since power sets can then be obtained (using limited ∆ 0 -replacement) from sets of functions into a 2-element set. Hence classical logic is also impredicative. Also considered impredicative is: Full separation and ∆ 0 -classical logic together imply full classical logic, since we can form a = { ∅ | ϕ } ⊆ { ∅ }, and then (∅ ∈ a) ∨ (∅ ∈ a) is an instance of ∆ 0classical logic that implies ϕ∨¬ϕ. A similar argument shows that ∆ 0 -classical logic is equivalent to the assertion that every subset has a complement. We also have the collection and replacement axioms.
• Collection: for any formula ϕ(x, y), for any a, if for all x ∈ a there is a y with ϕ(x, y), then there is a b such that for all x ∈ a, there is a y ∈ b with ϕ(x, y), and for all y ∈ b, there is a x ∈ a with ϕ(x, y) . • Replacement: for any formula ϕ(x, y), for any a, if for every x ∈ a there exists a unique y with ϕ(x, y), then the set { y | (∃x ∈ a)ϕ(x, y) } exists .
With an evident extension of Definition 2.3 to formulas, we can state the collection axiom as "if ϕ is entire on a, then there exists b such that ϕ is bi-entire from a to b." Collection also evidently implies replacement. Classical ZF set theory is often defined using replacement rather than collection, but in the presence of the other axioms of ZF, collection can be proven. (Replacement and full classical logic together also imply full separation.) This is no longer true in intuitionistic logic, though, or in classical logic without the axiom of foundation, and in practice the extra strength of collection is sometimes important. There are also other versions of collection, all of which are equivalent in the presence of full separation, but the one we have chosen seems most appropriate in its absence. We consider only the version of the axiom of infinity which asserts the existence of the set ω of finite von Neumann ordinals.
• (von Neumann) Infinity: there exists a set ω such that ∅ ∈ ω, if x ∈ ω then x ∪ {x} ∈ ω, and if z is any other set such that ∅ ∈ z and if x ∈ z then x ∪ {x} ∈ z, then ω ⊆ z .
We can omit the final clase in this axiom in the presence of power sets or full separation, since it can be recovered by replacing ω with its smallest subset containing ∅ and closed under successor x → x ∪ {x}. But otherwise we need to include this clause explicitly, in order to prove that mathematical induction holds for ∆ 0 -formulas. For a stronger version of induction, we need a separate axiom.
Of course, infinity plus full separation implies full induction.
There are also various axioms of choice; we will consider only the following two.
• Choice: for any set a, if for all x ∈ a there exists a y ∈ x, then there exists a function f from a to a such that f (x) ∈ x for all x ∈ a .
• Presentation: For every set a, there exists a surjection b → a, where b has the property that any surjection c → b has a section.
By Diaconescu's argument [Dia75], choice and power set together imply ∆ 0 -classical logic. A set b as in the presentation axiom is called projective; thus the presentation axiom is also called "EPSets" (Enough Projective Sets) or "COSHEP" (the Category Of Sets Has Enough Projectives). It implies countable dependent choice. Finally, we have the family of "foundation-type" axioms. Recall that a set x is • Set-induction: for any formula ϕ(x), if for any set y, ϕ(x) for all x ∈ y implies ϕ(y), then ϕ(x) for any set x . • Foundation, a.k.a. ∆ 0 -set-induction: like set-induction, but only for ∆ 0 -formulas. • Transitive closures: every set is a subset of a smallest transitive set .
• Mostowski's principle: every well-founded extensional relation is isomorphic to a transitive set equipped with the relation ∈ .
The usual "classical" formulation of foundation is In the presence of transitive closures, regularity is equivalent to the conjunction of ∆ 0 -set-induction and ∆ 0 -classical logic. Thus, in an intuitionistic theory, ∆ 0 -setinduction is preferable. Of course, ∆ 0 -set-induction follows from full set-induction, while the converse is true if we have full separation. Set-induction also implies full ordinary induction, since < and ∈ are the same for von Neumann ordinals. Transitive closures can be constructed either from set-induction and replacement (see [AR01]), or from infinity, ordinary (full) induction, and replacement.
Mostowski's original proof shows that his principle follows from replacement and full separation. Transitive closures and Mostowski's principle are not usually considered "foundation" axioms, but we group them thusly for several reasons: • The conjunction of transitive closures, Mostowski's principle, and foundation is equivalent to the single statement "to give a set is the same as to give a wellfounded extensional relation with a specified element." One could argue that this sums up the objects of study of well-founded material set theory. • As we will see in §8, it follows that the (well-founded) material set theories that can be constructed from structural ones are precisely those which satisfy these three axioms. • Finally, the various axioms of anti-foundation are also naturally stated as "to give a set is the same as to give a (blank) relation with a specified element," where (blank) denotes some stronger type of extensionality (there are several choices; see [Acz88]). Thus, these axioms naturally include analogues not just of foundation, but also of transitive closures and Mostowski's principle.
Similar groupings can be found in, for instance, [ABSS14] and [Mat01]. Some particular material set theories with names include the following. Note that in this context, the prefix constructive is generally reserved for "predicative" theories (including, potentially, exponentiation and fullness, but never power sets or full separation) while intuitionistic refers to "impredicative" (but still non-classical) theories which may have power sets or full separation. None of these theories include our axiom of limited ∆ 0 -replacement explicitly, but all include either power sets or a stronger version of replacement, both of which imply it.
• The standard Zermelo-Fraenkel set theory with Choice (ZFC) includes all the axioms mentioned above, although it suffices to assume the core axioms together with full classical logic, power sets, replacement, infinity, foundation, and choice. • By Zermelo set theory (Z) one usually means the core axioms together with full classical logic, power sets, full separation, and infinity. • The theory ZBQC of [ML86], called RZC in [MLM94, VI.10] and BZC elsewhere, consists of the core axioms together with full classical logic, power sets, infinity, choice, and regularity. • By Intuitionistic BZ we will mean the core axioms together with power sets, infinity, and foundation. • The Mostowski set theory (MOST) of [Mat01] consists of ZBQC together with transitive closures and Mostowski's principle. • By Kripke-Platek set theory (KP) is usually meant the core axioms together with full classical logic, a form of ∆ 0 -collection (sufficient to imply our limited ∆ 0 -replacement), and set-induction for some class of formulas. • The theory ZFC− of [GHJ11] consists of the core axioms together with full classical logic, infinity, foundation, choice, and replacement (the "sufficient axioms" listed above for ZFC, with power sets removed), while their ZFC − has collection instead of replacement. (Actually, they use a version of choice that is stronger than ours in the absence of power sets, but is unsuitable intuitionistically.) • Aczel's Constructive Zermelo-Fraenkel (CZF) consists of the core axioms together with fullness, collection, infinity, and set-induction; see [AR01]. His CZF 0 consists of the core axioms, replacement, infinity, and induction. • The usual meaning of Intuitionistic Zermelo-Fraenkel (IZF) is the core axioms together with power sets, full separation, collection, infinity, and setinduction. This is the strongest theory that can be built from the above axioms without any form of classical logic or choice. • The Rudimentary Set Theory (RST) of [vdBM07] consists of the core axioms together with collection and set-induction. So far we have considered only theories of pure sets, i.e. in which everything is a set. If we want to also allow "atoms" or "urelements" which are not sets, we can modify any of the above theories by adding a predicate x is a set , whose negation is read as x is an atom . We must then add the following axiom: • Only sets have elements: if x ∈ y, then y is a set . and modify the extensionality axiom so that it applies only to sets: • Extensionality for sets: for any sets x and y, x = y if and only if for all z, z ∈ x iff z ∈ y . We may choose whether or not to add the following axioms: • Decidability of sethood: every x is either a set or an atom . • Set of atoms: the set { x | x is an atom } exists . as well as whether to allow the predicate x is a set to appear in the formulas that parametrize the axiom schemas. For instance: • The theory IZFA of [JM95] consists of IZF, as above, with atoms and decidable sethood, and does allow sethood in axiom schemas.
• If ZFA has a standard meaning, it is probably IZFA plus full classical logic.
• The Basic Constructive Set Theory (BCST) of [AW06,AFW06] consists of the core axioms together with replacement, with atoms. Their Constructive Set Theory (CST) adds exponentials to this, and the Basic Intuitionistic Set Theory (BIST) of [AF06, AFW06, ABSS07, ABSS14] adds power sets and a non-von-Neumann version of infinity. These theories do not assume decidability of sethood or a set of atoms, and do not allow sethood in axiom schemas. • The theory BIZFA of [ABSS14] consists of BIST, as above, together with decidable sethood, foundation, transitive closures, and Mostowski's principle (suitably modified for the existence of atoms), and does allow sethood in axiom schemas.

Heyting pretoposes
We now move on to structural set theories, beginning with the underlying logic. The theory of a category can, of course, be formulated in ordinary first-order logic, but this is unsatisfactory to us because it allows us to discuss equality of objects. However, we cannot simply remove the equality predicate on objects from the ordinary first-order theory, because sometimes we do need to know that two objects are the same. For example, to compose two arrows f and g, we need to know that the source of g is the same as the target of f . The solution (c.f. [Fre76,Bla79,Mak95,Mak01]) is to use a language of dependent types. We give here a somewhat informal description in an attempt to avoid the complicated precise syntax of dependent type theory, but the reader familiar with DTT should easily be able to expand our description into a formal one.
Definition 3.1. The language of categories consists of the following.
(i) There is a type of objects. By an object-variable we mean a variable that has been assigned to the type of objects. (ii) Each object-variable is, in particular, an object-term. (iii) For object-terms X and Y , there is a type X → Y of arrows from X to Y .
By an arrow-variable we mean a variable that has been assigned to some type of arrows (which entails specifying the object-terms X and Y ). (iv) Every arrow-variable is, in particular, an arrow-term. Like arrow-variables, every arrow-term is assigned to a particular type of arrows. (v) For each object-term X, there is an arrow-term 1 X : X → X. (vi) For any object-terms X, Y , and Z and each pair of arrow-terms f : X → Y and g : Y → Z, there is an arrow-term (g • f ) : X → Z. (vii) For any arrow-terms f, g : X → Y , there is an atomic formula (f = g). Non-atomic formulas are built up from atomic ones in the usual way, using connectives ⊤, ⊥, ∧, ∨, ⇒, ¬, and quantifiers ∃ and ∀. There are of course two types of quantifiers, for object-variables and for arrow-variables; the former is restricted in that we may not quantify over an object-variable if it appears in the type of any free arrow-variable.
Of course, this theory uses very little of the full machinery of DTT, and in particular it may be said to live in the "first-order" fragment of DTT. In this way it is closely related to the logic FOLDS studied in [Mak95], although we are allowing some term constructors in addition to relations.
Notation 3.2. We will use the same notational convention for free variables as in Notation 2.1, but adapted appropriately for dependent type theory. In particular, by a context in this language, we mean a finite (ordered) list Γ of typed variables, with the property that whenever an arrow-variable f : X → Y occurs in Γ, each of X and Y is an object-variable occurring in Γ prior to f . If Θ is a further list of typed variables which is an extension of Γ, in the sense that the concatenation (Γ, Θ) is a context, then we say that a formula written ϕ(Θ) is in context Γ if all its free variables are in (Γ, Θ).
Thus, for instance, Γ = (X, Y, f : X → Y ) is a context, and if g : X → Y is a further arrow-variable, then a formula whose free variables are among X, Y, f, g may be denoted ϕ(g) in context Γ.
Definition 3.3. Let A be a category, Γ a context, and let ρ be a well-typed assignment of the variables in Γ to objects and morphisms of A. We denote this by ρ : Γ → A. Then the satisfaction relation A ρ ϕ is defined as usual, by induction on the structure of ϕ. If ρ is obvious from context, we omit it from the notation.
The main thing to note about this language is that, as in FOLDS, the only atomic formulas are equalities between parallel arrows; the language does not allow us to even discuss whether two objects are equal. (However, we do still assume the usual rules of equality for equalities of arrows, such as substitution, reflexivity, symmetry, and transitivity.) This implies that satisfaction is isomorphism-and equivalence-invariant, in the following sense.
Lemma 3.5 (Equivalence-invariance of truth). If ϕ is a formula in context Γ, and the functor F , as above, is fully faithful and essentially surjective, then A ρ ϕ if and only if B F •ρ ϕ.
Both of these lemmas are proven by straightforward induction on the structure of ϕ. (In fact, the dependently typed theory of categories characterizes exactly those properties of categories which are invariant under equivalence in this sense; see [Bla79,Fre76,Mak95]. ) We now list the basic category-theoretic properties we will consider. First of all, we must have a category, so we include: Recall that a Heyting category is a category satisfying the following axioms.
• Finite limits: there exists a terminal object, binary products, and equalizers .
• Regularity: every morphism factors as a regular epi followed by a monic, and regular epis are stable under pullback . • Coherency: finite unions of subobjects exist and are stable under pullback .
• Dual images: for any f : has a right adjoint ∀ f . Of course, a statement such as binary products exist actually means for all X, Y , there exists W and p : W → X, q : W → Y such that for any T and a : The notation Sub(X) denotes the poset of subobjects of X, i.e. of monomorphisms into X modulo isomorphism. In order to remain first-order, the axiom of dual images should be interpreted as asserting the existence of each individual value of ∀ f with its universal property, i.e.
for any f : X → Y , and any monomorphism m : A → X, there exists a monomorphism n : B → Y such that for any monomorphism q : C → Y , we have that q factors through n if and only if there exists a pullback of q along f which factors through m . A Heyting category is called a Heyting pretopos if it also satisfies: • Positivity/extensivity: there exist binary coproducts which are disjoint and pullbackstable . • Exactness: every equivalence relation is a kernel . It is a Π-pretopos if it also satisfies: • Local cartesian closure: for every arrow f : X → Y , the pullback functor f * : S/Y → S/X has a right adjoint Π f Finally, if it additionally satisfies: • Power objects: every object X has a power object P X (which, together with finite limits, implies all the other axioms of a Π-pretopos) it is called an (elementary) topos. See, e.g., [Joh02, §A.1] for more details.
In a pretopos, every mono and every epi is regular, and thus it is balanced (every monic epic is an isomorphism). Furthermore, the self-indexing of any pretopos is a stack for its coherent topology. Of course, first-order versions of these statements can be proven, in the language of categories, from the above axioms.
Remark 3.6. Since all of our axioms are formulated in first-order logic, all the categorical operations such as finite limits, exponentials, etc. are expressed as pure existence statements. Strictly speaking this means that notation such as "A × B" or "X Y " is an abuse, since we have no product or exponential operations (and we are not assuming any axiom of choice allowing us to construct such operations). However, such abuses are standard in mathematics and cause no problems; formally they are no different from the notation { x | ϕ(x) } in material set theory, whose separation axioms are also formally expressed as pure existence statements. In fact, we could make this precise by extending our language to include such operations on terms and proving formally that it can still be interpreted in categories satisfying only the pure existence axioms (thereby moving in the direction of type theory), but we leave this to the interested reader.
Some other important axioms are the following: • Booleanness: every subobject has a complement .
• Enough projectives: Every object admits a regular epimorphism from an object which is projective with respect to regular epimorphisms. (In the absence of cartesian closure, the definition of an nno should be taken with arbitrary parameters; see [Joh02, A2.5.3]. On the other hand, since every epi is regular in a pretopos, we can omit any occurrences of the adjective "regular".) Each of the above axioms (beyond those of a Heyting pretopos) is, more or less obviously, a counterpart of some axiom of material set theory. This is perhaps least obvious in the case of Booleanness, which we regard as a structural counterpart of ∆ 0 -classical logic. However, in §2 we observed that in material set theory, ∆ 0classical logic is equivalent to the assertion that every subset has a complement. See also Lemma 4.4 and Proposition 5.2.
We end this section by observing that each material axiom implies its corresponding structural axiom for the category of sets.
Theorem 3.7. If V satisfies the core axioms of material set theory, then the sets and functions in V form a Heyting pretopos Set(V). Moreover: Proof. We first show that Set(V) is a category. Using pairing and limited ∆ 0replacement, we can form, for any set a and any x ∈ a, the set p a,x of all pairs {x, y} for y ∈ a. Again using limited ∆ 0 -replacement, we can form the set of all the p a,x for x ∈ a, and take its union, thereby obtaining the set of all pairs {x, y} for x, y ∈ a. Applying this construction twice to a ∪ b = {a, b}, we can then use ∆ 0separation to cut out the set a×b of Kuratowski ordered pairs (x, y) = {{x}, {x, y}} where x ∈ a and y ∈ b. With this in hand we can define function composition and identities using ∆ 0 -separation. Finite limits are straightforward: we already have products, {∅} is a terminal object, and ∆ 0 -separation supplies equalizers. The construction of pullback-stable images, unions, and dual images is also easy from ∆ 0 -separation. A stable and disjoint coproduct a + b can as usual be obtained as a subset of And if r ⊆ a × a is an equivalence relation, ∆ 0 -separation supplies the equivalence class of any x ∈ a, and limited ∆ 0 -replacement then supplies the set of all such equivalence classes.
Exponentiation clearly implies cartesian closedness. For local cartesian closedness, suppose given f : a → b and g : x → a. Then the fiber of Π f (g) → b over j ∈ b should be the set of all functions s : this can be cut out of x f −1 (j) by ∆ 0 -separation. Finally, the entire set Π f (g) can be constructed from these and limited ∆ 0 -replacement, since each element of each fiber is a subset of a × x.
The relationship between power sets and power objects is analogous. We have just recalled that ∆ 0 -classical logic implies every subset has a complement, and the implication for full classical logic is evident. Now suppose that V satisfies infinity and exponentials, and let ω be as in the axiom of infinity; we define 0 ∈ ω and s : ω → ω in the obvious way. Suppose We then prove by induction that for all n ∈ ω there exists an f ∈ Y with n ∈ dom(f ) and that for any two such f, f ′ we have f (n) = f ′ (n). The union of Y is then the desired function.
The presentation axiom, of course, is literally the statement that Set(V) has enough projectives. And finally, if V satisfies choice, then from any surjection p : e → b we can construct, using limited ∆ 0 -replacement, the set p −1 (x) x ∈ b , and applying the material axiom of choice to this gives a section of p.
Remark 3.8. We have stated Theorem 3.7 in the form "given a model of material set theory, we can construct a category with certain properties" because we find it easiest to conceptualize in that way. Of course, this requires the model of material set theory to exist in some ambient world in which we can perform this construction.
A more elementary way to interpret this "construction" is as giving a way to translate a formula ϕ in the language of category theory into a formula in the language of material set theory, by simply writing down what the assertion "ϕ holds in the category of sets" would mean in terms of the basic notions of set theory. The content of the theorem then becomes that if we assume certain axioms of material set theory, then the translations of certain category-theoretic axioms are provable-and therefore, so is any consequence of those axioms. (This is equivalent to performing the above model-theoretic construction with the generic model of a material set theory in its syntactic category.) In this way we can obtain a relative consistency result with the weakest possible metatheoretic assumptions. This same sort of interpretation will also be possible for the reverse construction in §8.
Remark 3.9. The proof of Theorem 3.7 is unaffected by the possible presence of atoms in V. This will remain true for the theorems in later sections giving similar correspondences for the other axioms.

Constructive well-pointedness
In §3 we considered only standard category-theoretic properties, but not every Heyting pretopos deserves to be called a model of structural set theory. The distinguishing characteristic of a set, as opposed to an object of some more general category, is that a set is determined by its elements and nothing more. This is expressed by the following property.    We immediately record the following. Proof. Functions 1 → X in Set(V) are in canonical correspondence with elements of X, and a function is monic just when it is injective. Thus, if m is monic and every map from 1 factors through it, then it must be bijective, and hence an isomorphism; thus 1 is a strong generator. Next, the epics in Set(V) are the surjections, and if X p −− ։ 1 is a surjection, then X must be inhabited, hence p splits. And if 1 = A∪B, then the unique element of 1 must be in either A or B by definition of unions, hence either A or B must be inhabited. Finally, ∅ has no elements, so 1 is nonempty.
Recall that classically, a topos is said to be well-pointed if 1 is a generator (i.e. for f, g : X ⇒ Y , having f x = gx for all 1 x −→ X implies f = g) and there is no map 1 → 0 (1 is nonempty). Thus, any constructively well-pointed topos is well-pointed in the classical sense. Conversely, the following is well-known (see, for instance, [MLM94, VI.1 and VI.10]).
Lemma 4.4. Let S be a Heyting category satisfying full classical logic, and in which 1 is a nonempty strong generator. Then S is Boolean and constructively well-pointed.
Proof. For any object X, either X is initial or it isn't. If it isn't, then there must be a global element 1 → X, since otherwise the monic 0 X would be an isomorphism (since 1 is a strong generator). Therefore, if X is not initial, then X → 1 is split epic. Now suppose that X is any object such that X → 1 is regular epic; since 0 → 1 is not regular epic, it follows that X is not initial, and so X → 1 must in fact be split epic; thus 1 is projective. Also, if 1 = A ∪ B, then A and B cannot both be initial, so one of them has a global element; thus 1 is indecomposable. Now let A X be a subobject and assume that A ∪ ¬A is not all of X. Then since 1 is a strong generator, there is a 1 Then V is a subobject of 1. If V is not initial, then it has a global element and hence is all of 1, so x factors through A ∪ ¬A. But if V is initial, then x * (A) must also be initial, which implies that x factors through ¬A. This is a contradiction, so A ∪ ¬A = X; hence S is Boolean.
Corollary 4.5. Let S be a topos satisfying full classical logic, which is well-pointed in the classical sense. Then S is Boolean and constructively well-pointed.
Proof. In a topos, any generator is a strong generator.
Thus, in the presence of full classical logic, our notion of constructive wellpointedness is equivalent to the usual notion of well-pointedness. However, Proposition 4.3 shows that a constructively well-pointed topos not satisfying full classical logic need not be Boolean. One can also construct examples showing that in the absence of full classical logic, a Boolean topos in which 1 is a nonempty generator need not be constructively well-pointed. It is true, however, even intuitionistically, that if 1 is projective, indecomposable, and nonempty in a Boolean topos, it must also be a generator; see [Awo97, V.3].
Remark 4.6. Other authors have also recognized the importance of explicitly assuming projectivity and indecomposability of 1 in an intuitionistic context. In [Awo97] a topos in which 1 is projective, indecomposable, and nonempty was called hyperlocal (but in [Joh92,Joh02] that word is used for a stronger, non-elementary, property). And in [Pal09], indecomposability of 1 is assumed explicitly, while projectivity of 1 is deduced from a factorization axiom. It is also worth noting that in an ambient classical logic, a Grothendieck topos is local, in the geometric sense that its global sections functor S(1, −) : S → Set has a right adjoint, if and only if 1 ∈ S is projective, indecomposable, and nonempty. See [SST + 17].
We note that most classical properties of a well-pointed topos make use of projectivity and indecomposability of 1, and many of these are still true intuitionistically as long as the category is constructively well-pointed. Proof. The "only if" part of (i) follows because 1 is projective. For the "if" part, note that a map p : Y → X in a regular category is regular epic iff its image is all of X, while if every 1 → X factors through p then it must factor through im(p) as well; hence im(p) is all of X since 1 is a strong generator.
The "only if" parts of (ii) are obvious. If f : Y → X is injective on global elements, then the canonical monomorphism Y → Y × X Y is bijective on global elements, and hence an isomorphism; thus Y is monic. And if f is bijective on global elements, then by this and by (i) it must be both monic and regular epic, hence an isomorphism.
The "only if" part of (iii) is also obvious. If every 1 → X which factors through A also factors through B, then in the pullback must be an isomorphism, since 1 is a strong generator; hence its inverse provides a factorization of A through B.
Finally, the "only if" part of (iv) is nonemptiness, while if X has no global elements, the map 0 → X is bijective on global elements, hence an isomorphism.
Remark 4.8. In terms of the internal logic, indecomposability of 1 corresponds to the disjunction property (if ϕ ∨ ψ is true, then either ϕ is true or ψ is true), while projectivity of 1 corresponds to the existence property (if (∃x)ϕ(x) is true, then there is a particular a such that ϕ(a) is true). We might also call nonemptiness of 1 the negation property (⊥ is not true).
By a structural set theory, we will informally mean an extension of the axiomatic theory describing a constructively well-pointed Heyting pretopos. Not many structural set theories have been given particular names, but here are a few. • Lawvere's Elementary Theory of the Category of Sets (ETCS), defined in [Law64], is the theory of a well-pointed topos with a nno satisfying full classical logic and the axiom of choice. • Palmgren's Constructive ETCS (CETCS), defined in [Pal09], is the theory of a constructively well-pointed Π-pretopos with a nno and enough projectives. • We will refer to the theory of a constructively well-pointed topos with a nno as Intuitionistic ETCS (IETCS).

Structural set theory as set theory
So far, we have expressed the axioms of structural set theory in a form familiar to category theorists. However, they can equivalently be formulated in a much more "set-theoretic" way, as was done in [Law05]. Besides its intrinsic interest, this reformulation facilitates the comparison with material set theories.
First of all, we formulate a structural counterpart of the notion of ∆ 0 -formula. For simplicity, we henceforth extend our language with a particular object-term "1", and modify the terminal-object axiom to assert simply that 1 is terminal . Now we define: • An arrow-variable x : 1 → X whose domain is 1 is a ∆ 0 -variable.
• A formula whose only atomic subformulas are ∆ 0 -atomic and whose only quantifiers are ∆ 0 -quantifiers is a ∆ 0 -formula. Note that a ∆ 0 -formula may contain non-∆ 0 free variables. We can now reformulate the basic structure of a Heyting category as a separation axiom.
Proposition 5.1. Let S be a category with finite limits in which 1 is a strong generator. Then the following are equivalent.
(i) S is a constructively well-pointed Heyting category.
(ii) S satisfies the schema of ∆ 0 -separation: for any ∆ 0 -formula ϕ(x) with free ∆ 0 -variable x : 1 → X, there exists a subobject S X such that any map x : 1 → X factors through S if and only if ϕ(x) holds .
Proof. First we assume (i) and prove (ii). As usual, in (ii) we are allowing ϕ to exist in an arbitrary context Γ, and the variables occurring in Γ are not restricted to be ∆ 0 . To make the induction go through, we prove a more general statement.
In addition to an arbitrary context Γ, we suppose Θ to be a ∆ 0 -extension of Γ (that is, Θ consists of ∆ 0 -variables and (Γ, Θ) is a context). Let ρ : Γ → S be a variable assignment, and let ρ(Θ) denote the product in S of the images under ρ of the codomains of all the ∆ 0 -variables in Θ. For example, if Θ = (x : 1 → X, y : 1 → Y ), then ρ(Θ) = ρ(X) × ρ(Y ). (If S does not have assigned products, we simply chose some such product.) Let ϕ(Θ) be a formula in context Γ; we will prove, by structural induction on ϕ, that there exists a subobject S ρ(Θ) such that t : 1 → ρ(Θ) factors through S if and only if ϕ(t) holds. This implies (ii) by taking Θ to be a singleton.
We begin by applying the pullback functor ρ(Θ) * : S → S/ρ(Θ) to ρ, obtaining a new variable assignment ρ Θ : Γ → S/ρ(Θ). Now for any variable x : 1 → X in Θ, the corresponding projection ρ(Θ) → ρ(X) induces a map The variable assignment ρ ′ Θ allows us to interpret each object-and arrow-term in context (Γ, Θ) in S/ρ(Θ). In particular, each ∆ 0 -term is interpreted by a morphism with domain ρ(Θ). If f and g are two such ∆ 0 -terms, we let f = g ρ(Θ) denote the equalizer of ρ ′ Θ (f ) and ρ ′ Θ (g). It is clear that t : 1 → ρ(Θ) factors through f = g if and only if (f = g)(t) holds. Now we can build up ϕ for all other formulas ϕ in the usual inductive way using the Heyting category structure of S, with intersections and unions interpreting ∧ and ∨, the Heyting implication for ⇒, images for ∃, and dual images for ∀. It is easy to verify, using all parts of the definition of constructive well-pointedness, that at each step the desired property is maintained.
Conversely, assume ∆ 0 -separation (ii) and that 1 is a strong generator. The argument of Lemma 4.7(ii) still applies to show that a morphism is monic iff it is injective on global elements. Let M denote the class of monics and E the class of morphisms that are surjective on global elements. Because 1 is a strong generator, any morphism in E is extremal epic (i.e. factors through no proper subobject of its codomain). Moreover, E is evidently stable under pullback.
For any map f : Y → X, apply ∆ 0 -separation to the formula (∃y ∈ Y )(f (y) = x) to obtain a monic m : S X. The pullback of m along f is a monic which is bijective on global elements, hence an isomorphism; thus f factors through m, and the factorization e : Y → S is in E by construction. Therefore, (E, M) is a pullbackstable factorization system, from which it follows that S is a regular category and that E is exactly the class of regular epics-and hence 1 is projective. Now given monics m : A X and n : B X, apply ∆ 0 -separation to the formula (∃a ∈ A)(m(a) = x) ∨ (∃b ∈ B)(n(b) = x) to obtain a monic S X. Lemma 4.7(iii) still applies to show that A ⊆ S and B ⊆ S and that if A ⊆ T and B ⊆ T then S ⊆ T ; thus S = A∪B. The defining property of S (it contains precisely those 1 → X factoring through either A or B) is evidently stable under pullback. Similarly, from the formula ϕ(x) = ⊥ we obtain a pullback-stable bottom element 0 X, so S is a coherent category. Moreover, by the construction of unions and empty subobjects, it follows that 1 is indecomposable and nonempty. Finally, dual images can similarly be constructed by applying ∆ 0 -separation to a formula with a universal ∆ 0 -quantifier.
Further categorical properties can also be reformulated in set-theoretic terms.
Proof. For a subobject S A, let ¬S A be the Heyting negation. By wellpointedness, x : 1 → A factors through ¬S if and only if it does not factor through S. Since x factors through S is ∆ 0 , giving ∆ 0 -classical logic every such x factors through S or ¬S; so by well-pointedness, S ∪ ¬S = A and S is complemented.
Conversely, if the category is Boolean, then any ∆ 0 -formula ϕ has a classifying subobject ϕ , and negation of formulas corresponds to the Heyting negation. Thus, if ϕ is complemented, ϕ ∨ ¬ϕ must be valid.
Proposition 5.3. A constructively well-pointed Heyting category is a topos if and only if it satisfies the following axiom: • for any X there is an object P X and a relation [∈ X ] X × P X such that for any S X, there exists a unique s : 1 → P X such that for all x : 1 → X, we have that x factors through S if and only if x, s factors through [∈ X ] .
Proof. The necessity of this axiom follows from the universal property of power objects. Conversely, assuming it, let R X × Y be any subobject. Using ∆ 0separation, let F Y × P X contain exactly those pairs y, s such that for all x : 1 → X, we have that x, y factors through R if and only if x, s factors through [∈ X ]. By the given axiom, for any y : 1 → Y there is a unique s : 1 → P X such that x factors through y * R if and only if x, s factors through [∈ X ], and this if and only if y, s factors through F . Therefore, since 1 is a strong generator, the projection F → Y is invertible, and so F defines a map f : Y → P X. By Lemma 4.7(iii), we have f * ([∈ X ]) ∼ = R, and uniqueness is likewise easy.
Proposition 5.4. A constructively well-pointed Heyting category is cartesian closed if and only if it satisfies the following axiom: • For any X and Y , there is an object Y X and an arrow ev : Y X × X → Y such that for any f : X → Y , there is a unique z : 1 → Y X such that for all x : Proof. Analogous.
We will see in Proposition 7.8 that in the presence of a structural replacement axiom, the axiom in Proposition 5.4 also implies local cartesian closure, just as with limited ∆ 0 -replacement and exponentiation in material set theory.
Remark 5.5. The expressive power of ∆ 0 -formulas depends on the other categorical structure that is present. For instance, in a cartesian closed category, morphisms f : X → Y are equivalent to morphisms 1 → Y X , so ∆ 0 -separation implies separation for formulas including quantifiers over arbitrary arrow-variables. Similarly, in a topos we can effectively quantify over subobjects of any A (that is, objects S equipped with a monomorphism S A) by quantifying over morphisms 1 → P A; the mono S A is determined only up to isomorphism by its classifying map 1 → P A, but by isomorphism-invariance (Lemma 3.4) this is invisible to our logic.
Convention 5.6. From now on we will use the following more "set-theoretic" terminology and notation for structural set theories. We write Set for the category in question, and call its objects sets and its arrows functions. We speak of morphisms 1 → X as elements of X, and we write x :∈ X to mean x : 1 → X. If f : X → Y is a function and x :∈ X, we write f (x) :∈ Y for f • x : 1 → Y . Similarly, we speak of monomorphisms S X as subsets of X and write S :⊆ X.
The notations :∈ and :⊆ are a hybrid of the familiar set-theoretic ∈ and ⊆ with the type-theoretic x : A. Unlike the former, but like the latter, they are not propositions of the theory that can be true or false, but rather typing judgments which indicate what sort of thing their left-hand argument is. By contrast, given x :∈ X and S :⊆ X, we write x ∈ S for the statement 1 x −→ X factors through S X , which is a proposition of the theory. Similarly, for S, T :⊆ X, we write S ⊆ T for the statement S X factors through T X .

Structural separation, fullness, and induction
There are several axioms from material set theory for which we have not yet considered structural versions. In this section, we consider full separation, fullness, and induction; in the next we consider collection and replacement.
The structural axiom of full separation simply generalizes Proposition 5.1(ii) to unbounded quantifiers.
• Separation: For any formula ϕ(x), for any set X, there exists S :⊆ X such that for any x :∈ X, we have x ∈ S if and only if ϕ(x) .
Lemma 6.1. If V satisfies the core axioms together with full separation, then Set(V) satisfies separation.
Proof. As observed in Remark 3.8, any formula ϕ in Set(V) in the language of categories may be translated into a formula ϕ in V in the language of material set theory. If V satisfies material separation, then S = { x ∈ X | ϕ(x) } has the desired property for structural separation.
The structural axiom of fullness is also a direct translation of the material one. • Fullness: for any sets X, Y there exists a relation R :⊆ M × X × Y such that R ։ M × X is regular epic, and for any relation S :⊆ X × Y such that S ։ X is regular epic, there exists an s :∈ M such that (s, 1) * R ⊆ S .
Lemma 6.2. If V satisfies the core axioms together with fullness, then Set(V) satisfies structural fullness.
Proof. Just like the proofs for exponentials and power sets in Theorem 3.7.
Remark 6.3. We have stated the axiom of fullness in a form referring explicitly to global elements, analogous to the axioms appearing in Propositions 5.3 and 5.4. Thus, unlike the properties of being a topos or being locally cartesian closed, this axiom is only suitable in a well-pointed category. However, by interpreting the above axiom in the stack semantics of [Shu18], we can obtain a fullness axiom that makes sense more generally. (In fact, it is exactly the categorical version of fullness from [vdBDM07,vdBM07], but lacking their 'smallness' conditions).
The axiom of induction, of course, only makes sense in the presence of the axiom of infinity. The structural axiom of infinity (existence of an nno) asserts that functions can be constructed by recursion, which implies Peano's induction axiom in the sense that any subset S :⊆ N which contains 0 :∈ N and is closed under s : N → N must be all of N . (The proof of Theorem 3.7(v) essentially shows that the converse holds in any Π-pretopos.) It follows from ∆ 0 -separation that ∆ 0formulas can be proven by induction; the axiom of full induction extends this to arbitrary formulas.
• Induction: For any formula ϕ(x) with free variable x :∈ N , where N is an nno, if ϕ(0) and (∀n :∈ N )(ϕ(x) ⇒ ϕ(sx)), then ϕ(x) for all x :∈ N . Just as in material set theory, infinity and full separation together imply full induction. We also have: Proposition 6.4. If V satisfies the core axioms of material set theory, and also the axioms of infinity, exponentials, and induction, then Set(V) has an nno and satisfies induction.
Proof. As in the proof of Lemma 6.1, any formula ϕ(x) in Set(V) with x :∈ N (where N = ω) can be rewritten as a formula in V, to which the material axiom of induction can be applied.
There is no particularly natural structural "axiom of foundation," although in §9 we will mention a somewhat related property. We can, however, formulate structural axioms which are closely related to the material axiom of set-induction.
• Well-founded induction: For any formula ϕ(x) with free variable x :∈ A, if A is well-founded under the relation ≺, and moreover if ϕ(y) for all y ≺ x implies ϕ(x), then in fact ϕ(x) for all x :∈ A . • Extensional well-founded induction: The same, but requiring A to also be extensional. These axioms are implied by separation, since then we can form { x :∈ A | ϕ(x) } and apply the definition of well-foundedness. We can also say: Proposition 6.5. If V satisfies the core axioms of material set theory, and also the axioms of set-induction and Mostowski's principle, then Set(V) satisfies extensional well-founded induction. If V additionally has power sets, then Set(V) satisfies wellfounded induction.
Proof. By Mostowski's principle, any extensional well-founded relation is isomorphic to a transitive set. Thus, set-induction performed over the resulting transitive set can be used for inductive proofs over the original well-founded relation. Finally, with power sets, any well-founded relation can be collapsed to a well-founded extensional one (an "extensional quotient" in the sense of §8).

Structural collection and replacement
We now turn to structural versions of the collection and replacement axioms. Various such axioms have been proposed in the context of ETCS (see [Law64,Col73,Osi74,McL04]), but none of these seem to be quite appropriate in an intuitionistic or predicative theory. Hence our axioms must be different from all previous proposals (though they are similar to the replacement axiom of [McL04]).
The intuition behind structural collection is that since the elements of a set in a structural theory are not themselves sets, instead of "collecting" sets as elements of another set we must collect them as a family indexed over another set. Also, since the language of category theory is two-sorted, it is unsurprising that we have to assert collection for objects and morphisms separately. In fact, we find it conceptually helpful to formulate three axioms of collection, although the third one is automatically satisfied.
Remember that all formulas exist in an unstated ambient context Γ. (In particular, the object-variable U in the first two axioms below must belong to Γ.) • Collection of sets: For any formula ϕ(u, X) with specified free variables u :∈ U and X, if for every u there exists an X with ϕ(u, X), then there exists a regular epi V p −− ։ U and an A in Set/V such that for every v :∈ V we have ϕ(pv, v * A) . −− ։ U such that p * f = p * g. We will abbreviate a formula ϕ(u, X, Y, f ) as in the axiom of collection of functions by ϕ(u, f ), with the object-variables X and Y implicitly present as the domain and codomain of f . We will say that Set "satisfies collection" if it satisfies all three of the above axioms. However, one, and sometimes two, of these are redundant. Proof. To show (i), let E e − → A be the equalizer of f and g and let S be the dual image ∀ a E, where A a − → U is the structure map of A as an object of Set/U . The assumption that u * f = u * g for every u :∈ U implies that every such u is contained in S. Since 1 is a strong generator, this implies S ∼ = U , and therefore E ∼ = A and so f = g; thus we can take V = U and p = 1 U .
To show (ii), let C = (B → U ) (A→U) be the exponential in Set/U , with projection C g −→ U . Then each c :∈ C corresponds to a map f c : (gc) * A → (gc) * B. Using the axiom of separation, find a subobject V m − → C such that c :∈ C is contained in V iff ϕ(f c ). By assumption, every u :∈ U lifts to some c :∈ V , so since Set is well-pointed, the projection V gm −− ։ U is regular epi. Finally, there is an evident map h : (gm) * A → (gm) * B such that ϕ(gmc, c * h) for all c :∈ V .
The appropriate structural formulation of the axiom of replacement is a bit more subtle. The idea is that if we modify the hypotheses of collection by asserting unique existence, then passage to a cover V ։ U should be unnecessary. As with collection, we may expect three versions for sets, functions and equalities. The second two of these are easy to state, and follow from collection.
By replacement of equalities, r * h = s * h. But the self-indexing of Set is a prestack, so h descends to g : A → B with p * g = h. Since p is regular epic, for any u :∈ U there is a v :∈ V with pv = u; thus u * h = v * p * h = v * g, whence ϕ(u, u * h).
These two replacement axioms imply, in particular, that universal properties are reflected by global elements. Rather than give a precise statement of this, we present a paradigmatic example.
Proposition 7.3. Let Set be a constructively well-pointed Heyting category satisfying replacement of functions, and suppose we have A, B, E in Set/X and a morphism v : Then v exhibits E as an exponential B A in Set/X.

Proof.
The assumption means that for any object C and any morphism f : C × x * A → x * B, there exists a unique g : C → x * E such that f = x * v • (g × 1). In particular, given any D in Set/X and morphism f : D × X A → B, for every x :∈ X there is a unique g x : (g × 1)). By replacement of equalities, f = v • (g × 1).
By the universal property of the exponential x * E, we have x * h = g x = x * g, and hence h = g by replacement of equalities.
Note that all such universal properties are automatically pullback-stable. We would also like an axiom of "replacement of sets," which would ensure that the existence of an object satisfying a universal property is also reflected by global elements. Since no structural theory can determine an object of a category more uniquely than up to unique isomorphism, one natural such statement would be: • Replacement of sets: if for every u :∈ U there is a set A with ϕ(u, A) which is unique up to unique isomorphism, then there is a B in Set/U such that ϕ(u, u * B) for all u :∈ U .
If Set is a pretopos (and in particular exact), then replacement of sets follows from collection by a proof analogous to that of Proposition 7.2, using the fact that in this case the self-indexing is a stack for the regular topology. Moreover, just as in material set theory, we have: Proposition 7.4. If S is a well-pointed Heyting category which satisfies full classical logic and replacement of sets, then it also satisfies full separation.
Proof. For any formula ϕ(x) with free variable x :∈ X, let ψ(x, A) be A is terminal and ϕ(x), or A is initial and ¬ϕ(x) . Since (∀x)(ϕ(x) ∨ ¬ϕ(x)) holds by classical logic, and initial and terminal objects are unique up to unique isomorphism, by replacement of sets we have a B in Set/X such that for any x :∈ X, if ϕ(x) then x * B is terminal, while if ¬ϕ(x) then x * B is initial. It follows that B → X is monic, and is the subobject classifying ϕ required by the separation axiom.
However, for most other purposes replacement of sets is basically useless, since hardly ever is a set determined up to absolutely unique isomorphism, only an isomorphism which is compatible with some additional functions whose existence is being asserted at the same time. For example, a cartesian product A× B is only determined up to an isomorphism which is unique such that it respects the projections A × B → A and A × B → B with which the product comes equipped.
In order to state a useful version of replacement, we recall the notion of context extension from Notation 3.2: if (Γ, Θ) is a context, then we can write ϕ(Θ) in context Γ if ϕ is a formula whose free variables all lie in (Γ, Θ). Since all contexts are finite, we can write formulas like there exists Θ. We will write Θ ′ for a context obtained from Θ by replacing all of its variables by fresh ones (hereafter denoted with primes, X → X ′ ), so that (Γ, Θ, Θ ′ ) is also a context. We write Φ Θ for a list of arrow-variables φ X : X → X ′ , one for each object-variable X in Θ; thus (Γ, Θ, Θ ′ , Φ Θ ) is also a context. Finally, we will write Φ Θ is an isomorphism Θ ∼ = Θ ′ for the formula ϕ(Θ, Θ ′ , Φ Θ ) in context Γ which asserts that (i) for every object-variable X in Θ, φ X is an isomorphism; and (ii) for every arrow-variable f : If X is in Γ rather than Θ, then φ X denotes the identity 1 X , and likewise for Y .
We can also talk about contexts and extensions of contexts in slice categories. A particularly important example is that the context (X, x :∈ X) can be instantiated in Set/U by the pair (U * U, ∆ U ) consisting of the object U * U = U × U and the morphism ∆ U : 1 U → U * U . Moreover, this pair is the universal such instantiation over U , in that for any u : 1 → U we have an isomorphism u * (U * U, ∆ U ) ∼ = (U, u). Similarly, for any V p −→ U we can consider (V * U, (1 V , p)), which has the analogous property that v * (V * U, (1 V , p)) ∼ = (U, pv) for any v : 1 → V .
Proposition 7.5. A constructively well-pointed Heyting category satisfying collection also satisfies collection of contexts: for any formula ϕ(U, u :∈ U, Θ) (in any context Γ, as always), • for every U , if for every u :∈ U there exists Θ extending (U, u) such that ϕ(U, u, Θ), then there exists a regular epi V p −− ։ U and a Θ ′ in Set/V extending (V * U, (1 V , p)) such that for every v :∈ V we have ϕ(U, pv, v * Θ ′ ) .
Proof. Simply apply collection of sets and functions repeatedly, using the fact that regular epimorphisms compose.
We can now improve "replacement of sets" to a more useful axiom.
• Replacement of contexts: for any formula ϕ(U, u :∈ U, Θ), for any U , if for every u :∈ U there is an extension Θ of (U, u) such that ϕ(U, u, Θ), and moreover this extension Θ is unique up to a unique isomorphism of contexts Φ Θ , then there is an extension Θ ′ of (U * U, ∆ U ) in Set/U such that ϕ(U, u, u * Θ ′ ) for all u :∈ U .
Proposition 7.6. Any constructively well-pointed Heyting pretopos satisfying collection also satisfies replacement of contexts.
Proof. By Proposition 7.5, there is a regular epi p : V ։ U and a Θ ′ in Set/V such that for every v :∈ V we have ϕ(U, pv, v * Θ ′ ). Let (r, s) : V × U V ⇒ V be the kernel pair of f , and consider r * Θ ′ and s * Θ ′ in Set/V × U V . The assumption implies that when pulled back along any z : 1 → V × U V , these two contexts become uniquely isomorphic. Thus, by replacement of functions and equalities applied some finite number of times, we actually have a unique isomorphism r * Θ ′ ∼ = s * Θ ′ in Set/V × U V . Uniqueness implies that this isomorphism satisfies the cocycle condition over V × U V × U V . Thus, since Set is a stack for its regular topology (applied some finite number of times), the entire context Θ ′ descends to some Θ ′′ in Set/U . Since p is surjective, the desired property for Θ ′′ follows.
I do not know whether replacement of contexts implies collection. But as in material set theory, replacement suffices in the classical world. Proof. By Propositions 7.1(ii), 7.4, and 7.6, it suffices to prove that replacement of contexts implies collection of sets. Given a formula ϕ(u, X), we can construct a context Θ including both a set X and a binary relation on it, and let ψ(u, Θ) assert that ϕ(u, X) holds and that the given relation is a well-ordering, which has the smallest possible order-type among well-ordered sets X such that ϕ(u, X).
Since classically, any set admits a smallest well-ordering which is unique up to unique isomorphism, we can apply replacement of contexts to ψ and thereby deduce collection of sets.
As promised, replacement of contexts implies that the existence of objects satisfying a universal property is reflected by global elements. Continuing the example of Proposition 7.3, we have the following.
Proposition 7.8. Let Set be a constructively well-pointed Heyting pretopos satisfying replacement of contexts. If Set is cartesian closed, then it is locally cartesian closed.
Proof. Let A, B be in Set/X; we want to construct the exponential (B → X) (A→X) . For x :∈ X, let ϕ(x, E, e) assert that e : E × x * A → x * B exhibits E as the exponential (x * B) x * A . This formula can be phrased as ψ(X, x, Θ) for some Θ, although we note that Θ involves not just E and e but also object-variables for x * A, x * B, and E × x * A, and arrow-variables giving the projections that exhibit these as two pullbacks and a cartesian product, respectively. Now, since Set is cartesian closed, for every x :∈ X there exists E and e with ϕ(x, E, e), and such are unique up to a unique isomorphism which respects all the structure. Therefore, replacement of contexts supplies an instantiation of Θ extending (X * X, ∆ X ) in Set/X. This consists essentially of an object C and a morphism c : C × X A → B. The conclusion of replacement of contexts implies that C and c satisfy the hypotheses of Proposition 7.3, so they must be an exponential (B → X) (A→X) as desired.
We end this section by extending Theorem 3.7 to the axiom of collection.
Theorem 7.9. If V satisfies the core axioms of material set theory along with collection, then Set(V) satisfies structural collection.
Proof. If V satisfies material collection, then given the setup of collection of sets for some formula ϕ, let ψ(u, X) assert that X is a Kuratowski ordered pair of the form (u, X ′ ) with ϕ(u, X ′ ). By material collection, let V be a set such that for any u ∈ U , there is an X ∈ V with ψ(u, X), and for any X ∈ V , there is a u ∈ U with ψ(u, X). Then every element of V is an ordered pair whose first element is in U , so there is a projection V → U , which by assumption is surjective. We can then form B = (u,X ′ )∈V X ′ , and by ∆ 0 -separation cut out Then A is an object of Set(V)/V , and for any v = (u, X ′ ) ∈ V , v * A is isomorphic to X ′ . Thus, by isomorphism-invariance, we have ϕ(u, v * A), as required. Collection of functions is analogous.
As far as I can tell, however, the material axiom of replacement does not seem to imply the structural axiom of replacement of contexts (in the absence of classical logic). This, I feel, is one of the reasons (though not the only one) that the material axiom of collection is necessary in practice. For example, it is well-known that while some types of "infinite iteration" can be performed in a topos with a nno, and consequently some sorts of "free structures" can be proven to exist (c.f. [JW78]), this is not always the case. However, infinite iteration (and more generally, transfinite iteration over a well-founded relation) is always possible in a well-pointed topos satisfying our structural axioms of induction and replacement. In [Shu18] we will see how to extend this observation to the non-well-pointed case.

Constructing material set theories
So far we have summarized the axioms of material set theory and structural set theory, and explained how most axioms of material set theory are reflected in structural properties of the resulting category of sets. We now turn to the opposite construction: how to recover a material set theory from a structural one. A "set" in material set theory, of course, contains much more information than a "set" in structural set theory, namely the membership relations between its elements, their elements, and so on. This gives rise to the idea of modeling a "material set" by a graph or tree with nodes depicting sets and edges depicting membership.
This basic idea was used by [Col73,Mit72,Osi74] in the first equiconsistency proofs of ETCS with BZC, and nearly identical constructions have been used for relative consistency proofs by others such as [Acz88] and [Mat01]. Here we perform essentially the same construction, but with an attention to details that ensures everything works in an intuitionistic or predicative context. For the rest of this section, we work in a constructively well-pointed Π-pretopos with an nno, denoted Set. I do not know whether an analogous construction can be made to work under weaker assumptions than this.
(i) A graph is a set X, whose elements are called nodes, equipped with a binary relation ≺. (ii) If x ≺ y we say that x is a child of y. (iii) A pointed graph is one equipped with a distinguished node ⋆ called the root. (iv) A pointed graph is accessible if for every node x there exists a path x = x n ≺ · · · ≺ x 0 = ⋆ to the root. (v) For any node x of a graph X, we write X/x for the full subgraph of X consisting of those y admitting some path to x. It is, of course, pointed by x, and accessible. "Accessible pointed graph" is abbreviated apg.
Remark 8.2. The hypothesis on Set is necessary to formalize "accessibility" and to define X/x. Specifically, a pointed graph X ≺ X × X with root ⋆ :∈ X is accessible if for every x :∈ X, there exists a nonzero finite cardinal [n] and a map [n] → X ≺ realizing a path from x to ⋆. (Recall that a finite cardinal is the pullback along a map 1 → N of the second projection N < → N of the strict order relation on the nno.) The definition of X/x is similar, using the fact that ∆ 0 -separation can be applied to functions in a Π-pretopos.
We are using the terminology of [Acz88]. The idea is that an arbitrary graph represents a collection of material-sets with ≺ representing the membership relation between them, a pointed graph represents a particular set (the root) together with all the data required to describe its hereditary membership relation, and an apg does this without any superfluous data (all the nodes bear some relation to the root). Thus, an arbitrary apg can be considered a picture of a possibly non-wellfounded set: the root represents the set itself, its children represent the elements of the set, and so on.
We will henceforth restrict attention to graphs for which ≺ is well-founded, thereby ensuring that the models of material set theory we construct satisfy the axiom of foundation. It is also possible, by changing this requirement, to construct models satisfying the various axioms of anti-foundation (see [Acz88]), but we will not do that here. Recall the definition: Definition 8.3. A subset S of a graph X is inductive if for any node x :∈ X, if all children of x are in S, then x is also in S. A graph X is well-founded if any inductive subset of X is equal to all of X.
In the presence of classical logic, well-foundedness is equivalent to saying that every inhabited subset of X has a ≺-minimal element, but in intuitionistic logic that version is too strong: Proposition 8.4. If there exists a graph X containing nodes u, v with u ≺ v, and such that every inhabited subset S :⊆ X has a ≺-minimal element (i.e. there exists an x ∈ S such that y ⊀ x for all y ∈ S), then excluded middle holds.
Proof. I learned this proof from Zhen Lin and Daniil Frumin. Let P be any proposition and let S = { y :∈ X | y = v ∨ (∃x)(x ≺ y ∧ P ) }. Then S is inhabited (by v), so it has a ≺-minimal element y. On one hand, if y = v, then ¬P , for if P then u ∈ S and so y would not be ≺-minimal in S. But on the other hand, if (∃x)(x ≺ y ∧ P ), then P .
Amusingly (and perhaps surprisingly), it follows that "classical well-foundedness" implies "inductive" well-foundedness even in the absence of classical logic: Corollary 8.5. If X is a graph in which every inhabited subset S :⊆ X has a ≺-minimal element, then it is well-founded.
Proof. Let S be inductive and x :∈ X; we want to show x ∈ S. Since S is inductive, it suffices to show that for any y ≺ x we have y ∈ S. But if y ≺ x, then by Proposition 8.4 excluded middle holds; thus X is well-founded, so S = X and hence x ∈ S.
We will say no more about classical well-foundedness. The intuitionistically correct Definition 8.3 of well-foundedness suffices to perform proofs by induction on a well-founded graph: by proving that a given subset is inductive, we conclude it is the whole graph. In order to prove a statement by well-founded induction, we must apply separation to the statement to turn it into a subset; thus either the statement must be ∆ 0 or we must have a stronger separation axiom. We can also use well-founded induction in more than one variable, since if X and Y are well-founded then so is X × Y .
We record some observations about well-founded graphs.
Lemma 8.6. Any subset of a well-founded graph is well-founded with the induced relation.
Proof. For any Z :⊆ X, if S :⊆ Z is inductive in Z, then the Heyting implication (Z ⇒ S) ⊆ X is inductive in X.
Lemma 8.7. If X is a well-founded graph, then there does not exist any cyclic path x = x n ≺ · · · ≺ x 0 = x in X.
Proof. If there were, then the Heyting complement of {x 0 , . . . , x n } ⊆ X would be inductive but not all of X.
Lemma 8.8. If X is a well-founded graph and x :∈ X, then x : 1 → X/x is a complemented subobject. In particular, it is decidable whether or not a node of a well-founded apg is the root.
Proof. By definition, every node y :∈ X/x admits some path to x, of length n :∈ N say. Since 0 is a complemented subobject of N , either n = 0, in which case y = x, or n > 0. If n > 0, then if x = y there would be a cyclic path from x to itself; hence in this case x = y. Thus for all y, either y = x or y = x, as desired.
Definition 8.9. We will write X x for the complement of x in X/x, i.e. the set of nodes admitting a path to x of length > 0. In particular, X ⋆ is the complement of the root.
We also need our apgs to satisfy the axiom of extensionality.
Definition 8.10. An graph X is extensional if whenever x and y are nodes such that z ≺ x ⇔ z ≺ y for all z, then x = y.
For non-well-founded graphs, this definition would have to be strengthened in one of various possible ways (see [Acz88]).
Remark 8.11. An equivalent characterization of the universe of extensional wellfounded apgs can be obtained by working with well-founded rigid trees instead. A tree is an apg in which every node x admits a unique path to the root, and it is rigid if for any node z and any children x ≺ z and y ≺ z, if X/x ∼ = X/y, then x = y. Every extensional well-founded apg X has an "unfolding" into a well-founded rigid tree X t , whose nodes are the paths in X, and conversely every well-founded rigid tree is the unfolding of some extensional well-founded apg. Rigid trees are used by [Col73,Mit72] and [MLM94], while extensional relations are used by [Osi74] and [Joh77], but they result in essentially equivalent theories. (In the non-wellfounded case, however, extensional relations seem more generally applicable than rigid trees; see [Acz88].) We now record some observations about extensionality and well-foundedness.
Definition 8.12. An initial segment of a graph X is a subset Y :⊆ X such that Lemma 8.13. Any initial segment of an extensional graph is extensional with the induced relation.
Lemma 8.14. If X is a well-founded extensional graph and X/x ∼ = X/y, then x = y.
In the language of [Acz88], Lemma 8.14 says that well-founded extensional graphs are "Finsler-extensional." Lemma 8.15. Any automorphism of a well-founded extensional graph is the identity. Therefore, any two parallel isomorphisms of well-founded extensional graphs are equal.
Proof. Let f : X ∼ − → X be an isomorphism; we prove by well-founded induction that f (x) = x for all x ∈ X. But if f (x ′ ) = x ′ for all x ′ ≺ x, then extensionality immediately implies f (x) = x.
Definition 8.16. We write V(Set) for the class of well-founded extensional apgs in Set.
Our goal is now to show that V(Set) is a model of a material set theory. We consider two apgs to be equal, i.e. to represent the same material-set, when they are isomorphic. And we model the membership relation ∈ in the expected way: Definition 8.17. If X is an apg, the children of its root are called its members. We write |X| for the set of members of X. If X and Y are apgs, we write X ǫ Y to mean that X ∼ = Y /y for some member y :∈ |Y |.
Here is our omnibus theorem.
Theorem 8.18. Let Set be a constructively well-pointed Π-pretopos with a nno, and let ϕ be a formula of material set theory. Then V(Set) ϕ whenever any of the following holds.
• Set is a topos and ϕ is the power set axiom.
• Set satisfies structural separation and ϕ is an instance of material separation.
• Set satisfies structural collection and ϕ is an instance of material collection.
• Set satisfies replacement of contexts and ϕ is an instance of material replacement. • Set is Boolean and ϕ is an instance of ∆ 0 -classical logic.
• Set satisfies full classical logic and ϕ is an instance of full classical logic.
• Set satisfies induction and ϕ is an instance of full induction.
• Set satisfies the axiom of choice and ϕ is the material axiom of choice.
• Set satisfies extensional well-founded induction and ϕ is an instance of setinduction.
Remark 8.19. As in Remark 3.8, we can also interpret this theorem as giving a translation of formulas in the language of material set theory into formulas in the language of structural set theory, and thereby obtain an equiconsistency result under weaker assumptions on the metatheory.
We will prove this theorem with a series of lemmas, but first we need to introduce some auxiliary notions leading up to the construction of extensional quotients.
Definition 8.20. Let X and Y be graphs. A simulation from X to Y is a function , then there exists an x ′ ≺ x with f (x ′ ) = y. A bisimulation from X to Y is a relation R :⊆ X × Y such that both projections R → X and R → Y are simulations (where R is considered as a full subgraph of X × Y ). A bisimulation is bi-entire if R → X and R → Y are surjective.
Note that if f : X → Y is a simulation, then the relation (1, f ) : X → X × Y is a bisimulation, which is bi-entire iff f is surjective.
An example of a simulation is the inclusion of an initial segment. The following lemma says that for extensional well-founded graphs, these are the only simulations.
Lemma 8.21. If X is well-founded and extensional, then any simulation f : X → Y is injective, and isomorphic to the inclusion of an initial segment.
Proof. We show by well-founded induction that f ( , so since f is a simulation there is a z 2 ≺ x 2 with f (z 2 ) = f (z 1 ). Hence z 1 = z 2 by induction, so z 1 ≺ x 2 . Dually, z 2 ≺ x 2 implies z 2 ≺ x 1 , so by extensionality x 1 = x 2 . Finally, any injective simulation must be an initial segment.
Lemma 8.22. If R is a bi-entire bisimulation from X to Y , then X is well-founded if and only if Y is so.
Proof. Suppose X is well-founded and S ⊆ Y is inductive. Let T :⊆ X consist of those x :∈ X such that R(x, y) implies y ∈ S; we show T is inductive. Suppose x :∈ X is such that x ′ ≺ x implies x ′ ∈ T , and that R(x, y). Then for any y ′ ≺ y there is an x ′ ≺ x with R(x ′ , y ′ ), whence x ′ ∈ T and thus y ′ ∈ S. So since S is inductive, y must be in S. Thus x ∈ T , so T is inductive. Since X is well-founded, T = X, and then since R is bi-entire, S = Y ; thus Y is well-founded.
Lemma 8.23. Any bi-entire bisimulation between extensional well-founded graphs must be an isomorphism.
Proof. Let R :⊆ X ×Y be such. We show by well-founded induction that if R(x, y 1 ) and R(x, y 2 ), then y 1 = y 2 . For if z 1 ≺ y 1 , then since R is a bisimulation, there is a w ≺ x with R(w, z 1 ), and again since R is a bisimulation, there is a z 2 ≺ y 2 with R(w, z 2 ). By induction, z 1 = z 2 , so that z 1 ≺ y 2 for any z 1 ≺ y 1 . By symmetry, for any z 2 ≺ y 2 we have z 2 ≺ y 1 , hence by extensionality y 1 = y 2 .
By symmetry, if R(x 1 , y) and R(x 2 , y) then x 1 = x 2 , so R is functional in both directions. Since it is also bi-entire, it must be an an isomorphism.
Lemma 8.24. If X is well-founded, then it is extensional if and only if every bisimulation from X to X is contained in the identity.
Proof. Suppose first X is well-founded and extensional and R is a bisimulation with R(x 1 , x 2 ). Then R is a bi-entire bisimulation from X/x 1 to X/x 2 (by ordinary induction on length of paths), so by Lemma 8.23 it must be an isomorphism X/x 1 ∼ = X/x 2 . But X is well-founded and extensional, so by Lemma 8.14, x 1 = x 2 . Now suppose that every bisimulation from X to X is contained in the identity, and also that x, y :∈ X are such that z ≺ x ⇔ z ≺ y for all z. Define R(a, b) to hold if either a = b, or a = x and b = y. Then R is a bisimulation, and if it is contained in the identity, then x = y; hence X is extensional.
In the language of [Acz88], Lemma 8.24 says that for well-founded graphs, extensionality is equivalent to "strong extensionality." Corollary 8.25. If Y is well-founded and extensional, then any two simulations f, g : X ⇒ Y are equal.
Proof. The image of (f, g) : X → Y × Y is a bisimulation, hence contained in the identity.
Therefore, well-founded extensional graphs and simulations form a (large) preorder. In the language of material set theory, this preorder represents the partial order of transitive-sets and subset inclusions.
Lemma 8.26. If X is a graph and R is a bisimulation from X to X which is an equivalence relation, then its quotient Y inherits a graph structure such that the quotient map [−] : X ։ Y is a simulation. Also, if X is an apg, then so is Y .
Proof. Define ≺ on Y to be minimal such that [−] preserves ≺, i.e. y 1 ≺ y 2 if there exist x 1 ≺ x 2 in X with [x 1 ] = y 1 and [x 2 ] = y 2 . Now suppose that y ≺ [x]. By definition this means that there exist z 1 ≺ z 2 with [z 1 ] = y and [z 2 ] = [x], i.e. R(z 2 , x) holds. But R is a bisimulation, so there exists x ′ ≺ x with R(z 1 , x ′ ), i.e. [x ′ ] = y; hence [−] is a simulation. If X is an apg, we define the root of Y to be [⋆]; accessibility of Y follows directly from that of X.
Of course, by Lemma 8.22, if X is well-founded, then so is the quotient Y . This gives us a way to construct extensional quotients in some cases.
Lemma 8.27. If Set is either a topos or satisfies full separation, then for every well-founded relation X there is a surjective simulation X ։ X where X is wellfounded and extensional, and an apg if X is.
Proof. Note that the union of any family of bisimulations is a bisimulation. More specifically, if we have a relation R :⊆ A × X × X such that for each a :∈ A the relation a * R :⊆ X × X is a bisimulation, then its image π A R :⊆ X × X is a bisimulation. If Set is a topos, then we can take A to be the set of all bisimulations (a subset of P (X × X)), obtaining thereby the largest bisimulation.
A largest bisimulation R, if it exists, is necessarily an equivalence relation, since the identity, R • R, and R −1 are all bisimulations as well and hence contained in it. Moreover, if X is its quotient as in Lemma 8.26, then any bisimulation S on X induces by pullback a bisimulation on X, which is contained in R, hence S is contained in the identity; thus by Lemma 8.24 Y is extensional. This completes the topos case. If instead Set satisfies full separation, then we can instead construct the largest bisimulation as the set of all (x, y) :∈ X × X such that there exists a bisimulation R from X to X with (x, y) ∈ R, and proceed similarly.
Without power sets or separation, it seems impossible to construct all extensional quotients, but we can still construct them in a useful amount of generality.
Lemma 8.28. Let n be a fixed external natural number, let X be a well-founded apg, and assume that X/x is extensional whenever x is a node that admits a path of length n to the root. Then there is an extensional well-founded apg X and a surjective simulation q : X → X.
Proof. The proof is by external induction on n. (We will only need this lemma for n ≤ 3, so the reader is encouraged not to worry too much about what this induction requires of the metatheory.) The base case is easy: since the root ⋆ admits a path of length 0 to itself and X ∼ = X/⋆, we can take X = X. Now suppose the statement is true for some n, and let X satisfy the hypothesis for n + 1. For any k, write X k for the set of nodes admitting a path of length k to the root. Let the relation R on X be defined by R(x, y) if there exists an isomorphism X/x ∼ − → X/y. (This can be constructed using ∆ 0 -separation and local exponentials in Set.) Then R is a bisimulation and an equivalence relation, so by Lemma 8.26 it has a quotient Y which is again a well-founded apg.
We claim that Y satisfies the hypothesis for n. Let y ∈ Y n and suppose that y 1 , y 2 ∈ Y /y satisfy z ≺ y 1 ⇔ z ≺ y 2 ; we must show y 1 = y 2 . Applying the simulation property inductively, we have y = [x] for x ∈ X n , and y i = [x i ] with x i ∈ X/x for i = 1, 2. By Lemma 8.8, for each i either x i = x or x i ∈ X/w i for some w i ≺ x. If x 1 = x and x 2 = x, then of course y 1 = [x 1 ] = [x 2 ] = y 2 . If x 1 = x and x 2 ∈ X/w 2 with w 2 ≺ x = x 2 , then there would be a cyclic path in X from x 2 to itself, contradicting Lemma 8.7. Hence the only remaining case is when x i ∈ X/w i with w i ≺ x for both i = 1, 2. Now this implies that w i ∈ X n+1 , so each X/w i is extensional, and thus so is each X/x i by Lemma 8.13. Therefore, by Lemma 8.21, the quotient map [−] : X → Y induces an isomorphism X/x i ∼ = Y /[x i ] = Y /y i . But z ≺ y 1 ⇔ z ≺ y 2 means that Y y 1 ∼ = Y y 2 , and hence (by Lemma 8.8) also Y /y 1 ∼ = Y /y 2 ; thus we also have X/x 1 ∼ = X/x 2 . Thus, by definition, R(x 1 , x 2 ), and so y 1 = [x 1 ] = [x 2 ] = y 2 .
We have shown that Y satisfies the hypothesis for n. Thus it has an extensional quotient Y , and so the composite X → Y → Y is an extensional quotient of X.
This also yields another hypothesis under which all extensional quotients exist.
Corollary 8.29. If Set satisfies well-founded induction and collection, then for any well-founded apg X there is an extensional well-founded apg X and a surjective simulation q : X → X.
Proof. For any well-founded apg X, we prove by induction on x :∈ X that the apg X/x admits a surjective simulation X/x ։ Y where Y is well-founded and extensional. (This requires the axiom of well-founded induction since the existence of such a Y is an unbounded quantifier.) The case x = ⋆ then yields the result.
Thus, suppose this is true for all y ≺ x, and let (X/−) be the transitive closure of ≺ restricted to X × |X/x|, regarded as an object of Set/|X/x|, so that y * (X/−) ∼ = X/y for any y ≺ x. By collection, we can find a surjection f : A ։ |X/x|, a pointed graph p : Y → A in Set/A (here "pointed" means we have a section s : A → Y over A), and a function g : f * (X/−) → Y in Set/A, such that for any a :∈ A, the pullback a * (g) is a surjective simulation X/f (a) ։ a * Y where a * Y is well-founded and extensional. Give Y + 1 the relation ≺ induced from Y with also s(a) ≺ ⋆ for all a :∈ A, where ⋆ is the new point added. Then Y + 1 satisfies the hypotheses of Lemma 8.28 with n = 1; let Z be its extensional quotient.
Define h : X/x → Z by sending x to the image of ⋆ :∈ Y + 1, and sending z ∈ X x to its image by g a , where a :∈ A is such that z ≺ f (a). This is welldefined since g then restricts to a surjective simulation X/z ։ Z/h(z), and there can be only one h(z) :∈ Z with this property by extensionality of Z.
We can now start verifying the axioms of material set theory.
Lemma 8.30. The axiom of extensionality holds. That is, two well-founded extensional apgs X and Y are isomorphic iff Z ǫ X ⇔ Z ǫ Y for all Z.
Proof. The "only if" direction is clear, so suppose that Z ǫ X ⇔ Z ǫ Y for all Z. Then for every x :∈ |X|, we have X/x ǫ Y , hence X/x ∼ = Y /y for some y :∈ Y . By Lemma 8.14, this y must be unique, and conversely as well; hence we have a bijection g : |X| ∼ − → |Y | such that for any x :∈ |X| there exists an isomorphism h x : X/x ∼ − → Y /g(x) (which must be unique, by Lemma 8.15). Define a relation R from X to Y such that R(a, b) holds if: (i) a = ⋆ and b = ⋆, or (ii) there exists x :∈ |X| such that a ∈ X/x, b ∈ Y /g(x), and h x (a) = b. Then R is a bi-entire bisimulation, so by Lemma 8.23 it is an isomorphism.
Lemma 8.31. The axioms of empty set, pairing, and union hold.
Proof. The empty set is represented by the apg with one node and no ≺ relations, which has no members.
If X and Y are extensional well-founded apgs, let Z = X + Y + 1 with ≺ induced from X and Y along with ⋆ X ≺ ⋆ and ⋆ Y ≺ ⋆, where ⋆ is the new point added. Since X and Y are extensional, Z satisfies the hypothesis of Lemma 8.28 with n = 1, and its extensional quotient represents the pair {X, Y }.
Finally, if X is an extensional well-founded apg, let X denote the subset of those x :∈ X such that x ≺ y ≺ ⋆ for some y, let Y be the subset of X consisting of those nodes admitting some path to a node in X , and define Z = Y + 1 with ≺ inherited from Y and with y ≺ ⋆ for each y ∈ X ⊆ Y , where ⋆ is the new element added. Then Z satisfies the hypotheses of Lemma 8.28 with n = 1, so it has an extensional quotient, which is the desired union X.
Proof. Let X and Y be extensional well-founded apgs, and consider the set For x :∈ |X| we write x for its image in (X ⋆) Z and x ′ for its image in |X| Z. Similarly, we write y for images in Y ⋆, (x, y) for images in the first copy of |X| × |Y |, (x, y) ′ for images in the second copy, and ⋆ for the final point. We define ≺ on Z as follows: • ≺ on X ⋆ and Y ⋆ is induced from X and Y . • x ≺ x ′ for all x :∈ |X|. • x ≺ (x, y) and y ≺ (x, y) for all y :∈ |Y |. • x ′ ≺ (x, y) ′ and (x, y) ≺ (x, y) ′ for all x :∈ |X| and y :∈ |Y |.
• (x, y) ′ ≺ ⋆ for all x :∈ |X| and y :∈ |Y |. It is straightforward to verify that Z is then a well-founded apg. Since X and Y are extensional, Z satisfies the hypothesis of Lemma 8.28 with n = 3. Its extensional quotient then represents the cartesian product of X and Y .
Henceforth, we will write X ⊗Y for the extensional well-founded apg constructed above, which represents the cartesian product of the material sets X and Y . We will also reuse the notations such as (x, y) ′ for the images of these elements in X ⊗ Y .
Proof. If X and Y are extensional well-founded apgs, define W = ((X ⊗ Y ) ⋆) + |Y | |X| + 1 with ≺ induced from X ⊗Y , along with (x, y) ′ ≺ f whenever f (x) = y and f ≺ ⋆ for any f ∈ |Y | |X| . Then W is a well-founded apg, which is in fact already extensional; we claim it represents the material function-set.
It is clear that if F ǫ W , then F ∈ V(Set) is a function from X to Y in the sense of material set theory. Conversely, from any F ∈ V(Set) which is a function from X to Y , consider the subset of |X| × |Y | determined by those (x, y) such that the Kuratowski ordered pair {{X/x}, {X/x, Y /y}} is ǫ F . This defines a function |X| → |Y | in Set, which therefore induces an f :∈ |W | such that F ∼ = W/f . Observe that in particular, we have shown that for X, Y ∈ V(Set), there is a 1-1 correspondence between functions |X| → |Y | in Set and isomorphism classes of apgs F ∈ V(Set) which represent functions from X to Y in the sense of material set theory. In fact, although V(Set) need not satisfy limited ∆ 0 -replacement, so that Theorem 3.7 does not apply to it directly, we still have: Lemma 8.34. The sets and functions in V(Set) form a category Set(V(Set)), which can be identified with a full subcategory of Set closed under finite limits, subsets, quotients, and local exponentials. In particular, Set(V(Set)) is a Π-pretopos.
Proof. We have observed closure under products and non-local exponentials. Closure under subsets is easy: if U :⊆ |X|, then the sub-graph Y of X consisting of the root and all nodes admitting a path to U is a well-founded extensional apg with |Y | ∼ = U . This then implies closure under finite limits.
For quotients, if R is an equivalence relation on |X|, let q : |X| → Y be the quotient of |X| by R in Set; then the apg Z = (X ⋆) + Y + 1, with ≺ inherited from X along with x ≺ q(x) and y ≺ ⋆ for all x :∈ |X| and y :∈ Y , is well-founded and extensional and has |Z| ∼ = Y .
Finally, given f : |A| → |B| and g : |X| → |A|, we have the local exponential h : Π f (g) → |B| in Set, with counit e : Π f (g) × |B| |A| → |X|. Let Z represent the material cartesian product of A and X as in Lemma 8.32, and consider the apg with ≺ inherited from X ⊗ Y , along with (x, y) ′ ≺ j whenever f (x) = h(j) and e(j, x) = y, and j ≺ ⋆ for all j ∈ Π f (g). Then W is well-founded and extensional and satisfies |W | ∼ = Π f (g); hence Set(V(Set)) is closed under local exponentials. Proof. Analogously to exponentiation, if R :⊆ M × X × Y is a generic set of multi-valued functions from |X| to |Y |, consider x, y) and m ≺ ⋆ for all m :∈ M . Then W is a well-founded apg and satisfies the hypothesis of Lemma 8.28 with n = 1. Its extensional quotient represents a generic set of multivalued functions, by a similar argument as for exponentiation.
Lemma 8.36. If Set is a topos, then V(Set) satisfies the power set axiom, and the inclusion Set(V(Set)) ֒→ Set is a logical functor.
Proof. For an extensional well-founded apg X, define Y = (X ⋆) + P |X| + ⋆ with ≺ induced from X along with x ≺ A whenever x :∈ |X|, A :∈ P |X|, and x ∈ A; and also of course A ≺ ⋆. This is an extensional well-founded apg that represents the material power set of X. The second statement is immediate.
Lemma 8.37. V(Set) satisfies the axiom of infinity.
Proof. Let ω = N + 1, with ≺ defined to be < on N together with n ≺ ⋆ for all n ∈ N . This is an extensional well-founded apg which represents the von Neumann ordinal ω. The infinity axiom follows from the universal property of the nno. Proof. Let X be a well-founded extensional apg such that X x is inhabited for each x :∈ |X|. If Y :⊆ X × |X| consists of those (y, x) such that y ∈ X x, then the projection Y → |X| is surjective, and hence has a section, say s. From s we can easily construct a material choice function for X.
I do not know any way to show that having enough projectives in Set implies the presentation axiom for V(Set); the problem is that a projective object in Set seemingly need not admit any structure of a extensional well-founded apg.
Lemma 8.39. Set has transitive closures. therefore extensional and accessible. It follows that B + 1, with s(v) ≺ ⋆ for all v ∈ V , satisfies the hypotheses of Lemma 8.28 with n = 1. Its extensional quotient is then the set desired by the material collection axiom.
Lemma 8.44. If Set satisfies replacement of contexts, then V(Set) satisfies material replacement.
Proof. Suppose that A ∈ V(Set) and that ϕ is a formula such that for any X ǫ A, there exists a unique Y ∈ V(Set) with ϕ(X, Y ). Thus, for any x :∈ |A|, there exists a well-founded extensional apg Y such that ϕ ǫ (A/x, Y ), and any two such Y are isomorphic. Since any such isomorphism is unique by Lemma 8.15, replacement of contexts in Set supplies a pointed graph B in Set/|A| such that for each x :∈ |A| we have ϕ ǫ (A/x, x * B). The extensional quotient of B + 1 then represents the set desired by material replacement.
Lemma 8.45. If Set satisfies full induction, then so does V(Set).
Proof. If ϕ(x) is as in the statement of the material induction axiom, then ϕ ǫ (X) is a statement about some X ǫ ω, i.e. X ǫ N . But every X ǫ N is isomorphic to N/n for a unique n :∈ N , so ϕ ǫ (X) is equivalent to a statement ϕ ′ ǫ (n) about some n :∈ N , which can then be proven by the structural induction axiom.
Lemma 8.46. If Set satisfies extensional well-founded induction, then V(Set) satisfies set-induction.
Proof. Just like Lemma 8.45, using induction over the extensional well-founded relation in Set that underlies any object of V(Set).
For the schemata involving ∆ 0 -formulas, we require a different translation. Suppose ϕ is a ∆ 0 -formula in a material context Γ = (x 1 , . . . , x k ). Let Θ denote the structural context (U, R, i 1 : R → U, i 2 : R → U ), regarded as the data of a set with a binary relation which we denote ≺. We define a structural ∆ 0 -formula ϕ ∆0 ǫ in the context Γ ∆0 ǫ = (Θ, x 1 , . . . , x k ), where each x i is now regarded as a ∆ 0 -variable 1 → U . The translation is as follows.
• Each variable x i is unchanged.
• We replace the symbol = by equality of ∆ 0 -terms 1 → U .
• We replace the symbol ∈ by the relation ≺ on elements of U .
• The connectives are unchanged.
Now let ρ : Γ → V(Set) be a variable assignment in material set theory; thus it supplies well-founded extensional apgs ρ(x 1 ), . . . , ρ(x k ) in Set. Then ρ(x 1 ) + · · · + ρ(x k ) + 1, with ≺ inherited from the A i along with ⋆ i ≺ ⋆ for all 1 ≤ i ≤ k, satisfies the hypothesis of Lemma 8.28 with n = 1. Let T denote its extensional quotient, and let ρ ∆0 ǫ : Γ ∆0 ǫ → Set be the structural context which assigns U to T with its induced binary relation ≺, and each x i to [⋆ i ]. Proof. Lemma 8.14 implies that T /x ∼ = T /y if and only if x = y. Similarly, if T /x ǫ T /y, then T /x ∼ = (T /y)/y ′ = T /y ′ for some y ′ ≺ y, whence x = y ′ and so x ≺ y. The converse is easy, so T /x ǫ T /y if and only if x ≺ y. Thus the atomic formulas correspond, and the connectives evidently do, so it remains to observe that ∆ 0 -quantifiers are adequately represented by quantifiers over T , since by definition X ǫ T /y if and only if X ∼ = T /x for some x ≺ y.
Proof. Just like Lemma 8.41, but using ϕ ∆0 ǫ instead of ϕ ǫ , and the ∆ 0 -separation property of Proposition 5.1 instead of the separation axiom. Proof. For any ∆ 0 -formula ϕ in V(Set) and any well-founded apg X ∈ V(Set), we can form { x :∈ X | ϕ(X/x) } using ∆ 0 -separation, since ϕ(X/x) ⇔ ϕ ∆0 ǫ (x). The hypothesis on ϕ implies that this is an inductive subset of X, hence all of it. This implies the desired conclusion, since for every extensional well-founded apg Y there is another one X with Y ǫ X.
A-graphs. The resulting material set theories satisfy the modified axioms for theories with atoms listed at the end of §2, including decidability of sethood and the existence of a set of atoms (namely, A), and do allow sethood in axiom schemas.
Remark 8.55. The ability to use any object A of our category Set as "the set of atoms" means that when working with any fixed finite collection of objects in Set, we are free to use material set-theoretic language. However, there seems to be no structural way to construct a single model of material set theory which contains the elements of all the objects of Set as atoms, since without a way to compare objects for equality, we cannot compare their elements for equality. In [ABSS14], it is shown that this is the only obstruction: if we do have a way to interpret equality on objects ("internally" to Set), then such a model can be constructed.

Material-structural equivalences
Of course, it is natural to ask to what extent the constructions V(−) and Set(−) are inverse. We have already noticed the canonical inclusion Set(V(Set)) ֒→ Set, and the following is easy to verify.
Lemma 9.1. The inclusion Set(V(Set)) ֒→ Set is an equivalence if and only if every object of Set can be embedded into some extensional well-founded graph.
I propose to call this property of Set the axiom of well-founded materialization.
(Other axioms of materialization would arise from using various kinds of non-wellfounded graphs.) Note that well-founded materialization follows from the axiom of choice, since then every object can be well-ordered and thus given the structure of an apg representing a von Neumann ordinal. We remark in passing that this implies that "all replacement schemata for ETCS are equivalent." Proposition 9.2. Let T 1 and T 2 be axiom schemata for structural set theory such that for each i = 1, 2, (i) if V satisfies ZFC, then Set(V) satisfies T i , and (ii) if Set satisfies ETCS+T i , then V(Set) satisfies ZFC.
Then T 1 and T 2 are equivalent over ETCS.
Proof. Since ETCS includes AC, for any model of ETCS we have Set ≃ Set(V(Set)). Thus, if Set T 1 , then by (ii) we have V(Set) ZFC, hence by (i) we have Set = Set(V(Set)) T 2 . The converse is the same.
We have seen that our axioms of collection and replacement from §7 satisfy (i) and (ii), so over ETCS they are equivalent to any other such schema. This includes the reflection axiom of Lawvere [Law64,Remark 12], the axiom CRS of Cole [Col73], the axiom RepT of Osius [Osi74], and the replacement axiom of McLarty [McL04]. However, our axioms seem to be more appropriate in an intuitionistic context.
Returning to the material-structural comparison, on the other side we have: Proposition 9.3. If V satisfies the core axioms of material set theory along with infinity, exponentials, foundation, and transitive closures, then there is a canonical embedding V → V(Set(V)). This map is an isomorphism if and only if V additionally satisfies Mostowski's principle.
Proof. By assumption, any x ∈ V has a transitive closure TC(x), which is a wellfounded extensional graph. If we define Y = TC(x) + 1, with ≺ induced by ∈ on TC(x) and with z ≺ ⋆ for all z ∈ x, then Y is a well-founded extensional apg, i.e. an object of V(Set(V)). This construction gives a map V → V(Set(V)), and it is straightforward to verify that it preserves and reflects membership and equality. Now if this embedding is an isomorphism, then clearly V must satisfy Mostowski's principle, since V(Set(V)) does so. Conversely, if V satisfies Mostowski's principle, then every X ∈ V(Set(V)) is isomorphic in V to a transitive set, and therefore equal in V(Set(V)) to something in the image of the embedding.
We say that a material and a structural set theory are "equivalent" if we have a bijection between (i) isomorphism classes of models of the material set theory and (ii) equivalence classes of models of the structural set theory.
Corollary 9.5. ETCS plus structural collection (or replacement) is equivalent to ZFC.
Corollary 9.6. Intuitionistic ETCS plus well-founded materialization is equivalent to Intuitionistic BZ plus transitive closures and Mostowski's principle (which we may call "Intuitionistic MOST").
Corollary 9.7. Intuitionistic ETCS plus structural collection and well-founded materialization is equivalent to IZF.
Remark 9.8. The theory M 0 of [Mat01] consists of the core axioms together with power sets and full classical logic. If V M 0 , then V(Set(V)) is precisely the model W 1 constructed in [Mat01,§2], which satisfies M 0 plus regularity, transitive closures, and Mostowski's principle, and inherits infinity and choice from V. (In the presence of classical logic and power sets, the axiom of infinity is unnecessary for the construction V(−).) In particular, if V ZBQC, then V(Set(V)) MOST, while V(Set(V)) ∼ = V if we already had V MOST.
Remark 9.9. Mitchell [Mit73] observes that for Boolean topoi, the constructions we have called V(−) and Set(−) can be made into a pair of adjoint functors, modulo some 2-categorical technicalities not addressed therein. I expect this is also true in a constructive context. Moreover, the adjunction should be idempotent, and thus induce the above equivalences between the images of the two functors.