The n-Category Café

That’s funny — I think I’d always subconsciously imagined constructivists to be the sorts to rise before the sun and drink green tea. But I see from the timestamp on your comment that you really were up in the dark. I expect you typed your comment sitting in the lotus position:

(Novices may wonder how it is possible to type while in the lotus position. Ask a constructivist.)

In a way it’s a pity that the axiom of choice, applied to a well-pointed topos, implies that the topos is Boolean and two-valued. If it didn’t, we’d have to state those axioms separately, which would mean that removing the axiom of choice wouldn’t disembowel the whole theory in the way that it currently does.

Regarding “section” versus “right inverse”, I definitely see your point. I struggled with this one for a while. In the end, I went for “right inverse” because I think it’s more widely understood than “section”. (Would you agree? I don’t actually have any evidence.) But yes, “section” is definitely superior terminology. Apart from anything else, I usually can’t remember whether it’s a left or a right inverse that a non-injective surjection might plausibly have — it takes me a few moments to work it out. “Splits” is another possibility, though again it’s less widely understood than “right inverse”.

In general, where there’s been a choice about presentation (as in Karol’s question below), I’ve made the choice that I think will be most immediately appealing to the largest number of people.

Every math grad student at U.C. Riverside learns what an ‘inverse image’ is. Only students working on category theory have heard the word ‘equalizer’.

I suspect Tom is trying to make things immediately attractive to lots of people, rather than just people who already understand category theory. That seems like a wise objective, but I guess it’s important to state ones objective in foundational projects, since different objectives lead to different notions of success.

I hope the math community has reached the point of realizing that we really need not one foundation of mathematics, but many, together with clearly described relations between them. Indeed at this point the word ‘foundation’ is perhaps less helpful than something else… like maybe ‘entrance’.

I think the objection that ZFC requires everything to be a set is basically just a technicality;

That’s true and I can see how this leads people to conclude that there is no significant difference between so called material and structural set theories. However, I believe that this is only a symptom of a deeper “problem”. Namely, set theories like ZFC or ZFC with atoms force us to carry out many constructions by hand, for example in order to define products we need to introduce a particular notion of an ordered pair. There are many choices of such a definition, none more canonical than the others. Of course we can make this choice, prove the universal property of products and then forget our choice for all eternity. But having to make this choice in the first place is a distraction and distractions of this type happen all the time, for example in the classical construction of the progression of algebraic structures $\mathbb{N}$, $\mathbb{Z}$, $\mathbb{Q}$, $\mathbb{R}$. Structural set theory like ETCS allows us to assert that all the objects with expected universal properties exist without going into irrelevant details of their implementations which reduces the number of distractions.

Admittedly, those are not real “problems”. Those are merely “inconveniences” which are only inconvenient to people who are used to doing things in particular ways (e.g. defining things by their universal properties whenever possible).

You can get from a model of ZF plus a specified set of atoms to a model of ZFA, which is why Zermelo dropped atoms from his original axioms, but going the other way is not so simple.

But is there any way to build mathematics in ZFA in such a way that all the mathematical objects that we don’t think of as sets, such as $\pi$, end up being atoms? I can’t think of any way to, say, define the real numbers in ZFA, other than with the usual constructions, in which they end up being sets. There are atoms in ZFA, but since they don’t have any structure given on them, they don’t seem to participate in mathematics.

Of course, you could use the axiom of choice to pick a particular set of atoms which is bijective to the set-constructed real numbers (assuming you have sufficiently many atoms), transport all the structure of the real numbers across that bijection, and then declare that your set of atoms is now “the real numbers”. But that is starting to smell to me like a kludge, kind of like Bourbaki’s tedious definition of what kinds of set-theoretic baggage a “structure” is not allowed to refer to, or the comment of McLarty’s character Tasha that “the advantage of your set theory is that mathematicians never work with your sets!”.

Moreover, if you did that same procedure with every set whose elements you don’t want to think of as sets, then you would have to keep choosing new disjoint sets of atoms forever — unless you want it to be the case that perhaps $\pi$ is equal to a point on the torus, which is another instance of the same problem. In other words, you can get away from a global membership predicate by working with atoms, but you also have to worry about getting away from a global equality predicate, which is just as meaningless.

[P.S. I agree that it would be good to have more explanation of the text formatting options, but fortunately unless and until that happens there is google.)

Terry, you can find some information on the various text filters here. I generally use “itex to ML with parbreaks” as my filter. The HTML command <a href=”http://ncatlab.org/nlab/show/ZFA”>(http://ncatlab.org/nlab/show/ZFA)</a> should work to give you (http://ncatlab.org/nlab/show/ZFA), at least in this filter.

Terry wrote:

I think the objection that ZFC requires everything to be a set is basically just a technicality; one can simply move from ZFC to ZFC with atoms

I don’t dispute that one can introduce atoms or urelements (though it seems that Mike is not persuaded that it can be done in a way that reflects ordinary mathematical practice).

What I’d like to ask is: why would one want to choose this option, with its accompanying technicality, over the other options on offer? In particular, what reasons might one have for preferring it to the theory (due to Lawvere) described in my draft?

An aside: I was not able to figure out how to use HTML in comments. Presumably the mysterious “Text filter” options are relevant

Yes, sorry. That aspect of the site could definitely be improved, and I think you’ve remarked on this before. Since you’re familiar with MathOverflow, I suggest that you always choose the second option, “Markdown with itex to MathML”. This allows you to write things pretty much as you would do there.

the two theories are equiconsistent and, in fact, biinterpretable, but not equivalent.

They are equivalent in the following sense:

• If you start from a model of ZFC, build a model of ETCS+R, and then build a model of ZFC from that, you obtain a model that is isomorphic to the one you started with.

• If you start from a model of ETCS+R, build a model of ZFC, and then build a model of ETCS+R from that, you obtain a model that is an equivalent category to the one you started with.

What more would you ask for?

I think replacement is essential for ETCS to be considered as a robust foundational theory.

Tom makes a good argument in the paper that mathematicians almost never use replacement. But it sounds like you’re saying instead that mathematicians need separation and replacement in order to believe that a theory of sets “captures their intuitive notion of set”?

ETCS does, of course, include separation: you just have to prove it rather than taking it as an axiom. It’s a “bounded” separation by default, but it’s not hard to add an unbounded version if you want it. SEAR includes (unbounded) separation as a basic axiom, as well as a collection axiom. In this paper I considered the unbounded separation axiom for ETCS-like theories, and also what I think are the right “collection axiom” and “replacement axiom” in those formulations.

Thanks very much, François. I’m really glad to have your comments in particular.

(That might just sound like me obeying my own pleas for politeness, but actually I mean it.)

As you guessed, I didn’t mean “equivalence” in the precise sense that you had in mind: I was being somewhat vague. (In fact, I wasn’t aware of that precise usage.) I’ll have to reword it.

I’m not sure I understand what you say about replacement. As you know, ETCS has the logical strength of Zermelo set theory with bounded comprehension and choice. For a long time, people in category theory have been saying things like “no more than ETCS is needed anywhere in undergraduate mathematics”, though I don’t know of any places where such claims are written down, and I certainly can’t point to a written justification.

More recently, work of Colin McLarty, and I think also Angus Macintyre (?), seems to show that very large chunks of twentieth century mathematics can rest on ETCS as a set-theoretic foundation. I say “seems to” not to cast any doubt, but because this is way beyond my expertise, and (as you know) there was some scepticism expressed in response to this MathOverflow question.

This appears to suggest that bounded comprehension (i.e. ETCS) is enough for almost all purposes. Do you think that’s true? Of course, “almost all” is terribly vague, but let’s say “all the research that’s done in your department apart from logic and set theory”.

That’s not to deny, of course, that for a few purposes we might want to assume full replacement. But can’t we think of that as a kind of optional extra, in the same way that we might think of large cardinal axioms?

It’s a nitpick, but I also don’t favor the two-column format for anything I have to read online. For example, I don’t enjoy this feature that is to be found in anything appearing in the Notices of the AMS.

One last comment on the set vs function issue. I won’t add more since I think this issue is potentially too volatile. Thankfully, it hasn’t flared and I hope this comment will help keep it that way.

I think the issue is a cultural one, so there is no right and wrong, correct or incorrect, only differences. To me, in the broadest sense of the word, a set is a container with no distinguishing features other than its contents. Therefore, I think that a set theory must have an extensional membership relation. Anything goes after that, but extensionality is essential. So I do not think of ETCS and SEAR are set theories, though SEAR is interesting since it does not have equality for “sets”.

Mike and Tom are from a different culture and have a different perspective on what a set is. That is perfectly fine, I understand why that is and I respect their point of view. I do hope that I raised awareness of my point of view and that Tom will understand that ETCS might be more difficult to sell as a set theory for some. (I’m saying that because I do want people to buy into ETCS. It’s a very nice theory with very good potential!)

Mike wrote:

Of course, I’m a little biased, but I think that SEAR is also useful to consider

I agree! The current draft is dramatically slimmed down from earlier drafts. At one point it was 27 pages long; it’s now eight. The slimming process cut out a lot of things that I was rather attached to, including a passage about SEAR. So I’m glad you’ve brought it up here.

Is it possible that bounded ZF is consistent, but bounded ZFC is not?

No, ZF and ZFC are equiconsistent. This was shown by Gödel: in every model of ZF the constructible sets form a model of ZFC.

Hi Neel, nice to see you here!

Also, is axiom 3 really necessary?

Good point! I think you also need to invoke Axiom 4 to make sure $s^{-1}(0)$ is actually initial. This is worth looking into…

On a related note, you might want to explicitly show the construction of disjoint unions. Since it involves a double-powerset construction, I find it to be a surprisingly big hammer for cracking a rather small nut.

Yes, but that construction is absolutely fascinating!

The construction is much too long if done carefully, but I think it’s worth outlining it. Pointing out that $X$ and $Y$ embed disjointly into $P(X)\times P(Y)$ is easy. Since the existence of the union of two subobjects in ETCS is very believable, I think a parenthetical remark explaining that this is more complicated to prove in ETCS than one would think is enough.

It's pretty common that the axiom of empty set follows from the axiom of infinity; we have that in ZFC too. But I don't like removing empty set from the list. You don't want to tempt people to say things like ‘Finitist mathematics is useless, because without infinity, you don't even have the empty set.’.

Neel wrote:

is axiom 3 really necessary?

Yes. The terminal category is a model of the other 9 axioms, but it doesn’t satisfy Axiom 3. The sole purpose of this axiom is to outlaw that trivial model.

I don’t know what goes wrong if you attempt to deduce it from Axioms 7 and 9, but something must — unless you’ve just discovered an inconsistency.

On a related note, you might want to explicitly show the construction of disjoint unions.

I might, I might; I probably do! I think this is a really interesting point. But, like a diligent dieter, I’m struggling hard to keep my pagecount down, and this means restraining myself from indulging in too many interesting points. If I were going to do it at all, it would be a very quick summary along the lines that François suggests.

Thanks. I need to think about this whole right inverse/section terminology business, in the light of this conversation. What I had in mind was that “section” is most often used in the context of topology. (I see that Wikipedia appears to agree.) But anyway, thanks for alerting me to this bump in the road.

A good example! This is related to what I meant in my comment above by ‘using the wrong notion of family of sets’. Arguably, the ‘right’ notion of ‘I-indexed family of sets’ is not a formula expressing a relationship between elements of I and sets, but rather a function $p:X\to I$ (whose fibers are the sets being indexed). This (or something equivalent) is really the only sensible meaning if a ‘family of sets’ is to be a notion within the theory. Membership-based set theory is usually done with an uneasy marriage between notions in the theory, which are sets, and notions outside the theory (particularly first-order formulas), which forces you to use replacement to bridge the gap; categorical set theory promotes a cleaner point of view. (And type theory enforces a cleaner point of view.)

With this notion of ‘family of sets’ as the basis for a notion of ‘diagram’, it is immediate that every small (i.e. set-indexed) diagram has a limit and a colimit. The problem with $X \times PX\times PPX\times ...$ is then not that the limit doesn’t exist, but that the diagram doesn’t exist. This isn’t of course very different from how you described it as ‘countable yet large’, but I think it’s a slightly better point of view — there just is no such thing as a ‘large diagram on a small category’. This makes abstract category theory, for instance, a lot more comfortable.

I do agree, though, that that countable diagram should exist! But I’ve come to regard its nonexistence not so much in terms of a missing collection/replacement axiom, but in terms of an insufficiently powerful induction principle. For the natural numbers to be worthy of the name, you should be able to define anything you like recursively, including not just functions, but families of sets. (In type theory, the latter is called a ‘large elim’, and usually derived from the existence of a universe type, but it can also be postulated separately.)

what is the history behind right to left composition?

I don’t know. My impression is that the movement to reverse the convention, writing $(x)f$ or $x f$ instead of $f(x)$, was strongest in the early 1970s. I know there are some readers here who prefer it, but I imagine they feel quite lonely in that preference.

(You may have noticed that this corresponds to two different idioms for certain types of software. I first noticed it when I was using a “paint” type program as an undergraduate. In some such programs, you choose the tool [function] first and then the object to apply it to — e.g. choose “bucket fill” and then the area you’re filling. In others, it’s the opposite way round: object then function.)

1. I think the section “Why rethink?” doesn’t answer this question fully. What makes me feel uncomfortable whenever I think about foundations is, that there are plenty of statements which cannot be decided in ZFC.

Elsewhere on this thread, Mike evoked a helpful comparison between set theory and classical geometry, which I think makes the existence of undecidable statements seem less exotic. I also find it demystifying to consider the analogy (and more!) between undecidable statements and non-computable functions.

The “Why rethink?” bit was only about the disagreement between the meanings of “set” as used by most mathematicians and “set” as used in ZFC. It’s a somewhat subjective matter and I’m sure some people disagree with what I wrote, but to me it provides a good reason for “rethinking” — that is, finding an approach to set theory that reflects how mathematicians actually treat sets more accurately than ZFC does.

Since you need a weak version of AC for proving the existence of non-principle ultrafilters, does this mean, that the codensity of FinSet->Set is undecidable in ZF?

It’s provable without any form of choice that the codensity monad is the ultrafilter monad. The inclusion $FinSet \hookrightarrow Set$ is codense iff the codensity monad is the identity (more or less by definition), iff every ultrafilter is principal (by the previous sentence). Thus, $FinSet \hookrightarrow Set$ is codense iff every ultrafilter is principal. So, the answer to your question is yes.

As for the role of the number 3, I don’t have anything intelligent to say!

Thanks. I tinkered with the formatting for a long time, and I’m still not sure I like it: page 4 in particular (in the section you mention) looks messy.

For those subsection headings, I took my cue from newspapers, which sometimes split up long stories with centred, bold subheadings. Then again, I’ve seen magazines do the same thing but left-justified. Perhaps I’ll follow your suggestion and try that (again!).

Good question. It’s something I wondered about for a while (and ditto for axiom 8 and even axiom 3). My decision was not to, simply because it gets repetitive saying the same thing so many times. But I’m not sure I’ve made the right decision. I should think about it some more; thanks for flagging it up.

Materialistic structural set theory

Is material set theory vs structural set theory analogous to quantitative vs qualitative, or geometry vs topology? There are metric spaces, topological spaces and metrizable spaces. So what about material sets (or labelled sets), structural sets (or unlabelled sets) and materializable sets (or labelable sets). An atom is the same as a singleton lablelled set. Questions of membership and inclusion require labellings. What is a labelling? Is a labelling just a function from something to something? When does it make sense to talk about the automorphisms of a group if the elements aren’t labelled and relabelled? In “Combinatorial Species and Tree-like Structures” can the definition of species be extended to infinite sets. Would infinite species have anything to do with unifying structural and material viewpoints.

Sets are unstructured but surely “unstructure” is a form of structure in the same way that zero is a number or that a totally disconnected graph with no edges is still a graph.

From the “Back to Cantor?” post:

“find a reasonable unified foundation where structural sets and material sets happily live together as equals.”

Is an unlabelled set just a labelled set with the empty labelling?

Some quotes from “Species and Functors and Types, Oh My!” by Brent A. Yorgey:

“The theory of combinatorial species, although invented as a purely
mathematical formalism to unify much of combinatorics, can also
serve as a powerful and expressive language for talking about
data types.”

“The ability to relabel structures means that the actual labels we
use don’t matter; we get “the same structures”, up to relabeling,
for any label sets of the same size.”

“it is tempting to assume that labels play the role of the “data” held by data structures. Instead, however, labels should be thought of as names for the locations within a structure.”

“Although the formal definition of species is good to keep in mind
as a source of intuition, in practice we take an algebraic approach,
building up complex species from a small set of primitive species
and species operations.”

You seem to suggest that, in the ZFC view, you do know, or have some sense, of “what the sets are”. I would modify that notion, that you have names for lots of the sets, and imagine most of the rest as having generalized names in a similar way; but that most of your names for ZFsets are actually just fragments (on one side) of the $\in$ relation. Now, that may sound strange, except that when building models for exotic variations of ZF (or others) one frequently starts with a subclass or particular set and restricts the standard $\in$ to that — and it may well occur that the resulting $\in$-structure is not $\in$-transitive in the original universe, which means that the old names for everything in the new model are wrong with respect to the new model. This is one of those things set theorists do that most mathematicians need never worry about. Another such thing is to change the $\in$-relation of interest (as here).

On the other hand, there are plenty of basic (and suggestive) names for many sets in Tom’s presentation of ETCS; for instance, $\mathbf{0},\mathbf{1},\mathbf{2},\mathbb{N}$; and plenty of ways for building sets that fit in particular diagrams, such as $f^{-1}(z)$ whenever $f$ is the name for a function and $z$ is the name for a (possibly generalized) element of $f$’s codomain.

The theory has an ordinary first-order language formalization. Tom is just trying to provide an intuitive pedagogical presentation.

Max: there’s nothing hidden. The short answer (as Walt mentioned) is that this is a first order theory, just as ZFC is. The last paragraph of the introduction says a bit more along these lines. It sounds as if your points of confusion about this are really points of confusion over first order theories in general.

If you want to see a presentation of ETCS in pure logical syntax, here’s one by Colin McLarty. It’s not the same in every detail as mine, but it’s equivalent and it should give you the idea.

Walt goes a little further than I would: while I do hope I’ve conveyed some intuition and my paper is intended to be pedagogical, it’s also intended to be precise. It’s true that “some things” doesn’t sound precise, but I think it has exactly the same content as the corresponding formal logical expression.

If that doesn’t clarify things, I suggest the following. Don’t think of set theories (such as ZFC or this) as describing a world of sets that “exists” in some sense, because while you may indeed hold the opinion that they do exist, that leads into unnecessarily murky philosophical waters.

Instead, simply interpret them as a declaration of what the word “set” (and related words such as “element” and “function”) will be taken to mean. For example, if someone says “we will assume ZFC”, they’re really saying “I will use the words set and element to mean any things satisfying the ZFC axioms”. Ditto for ETCS, with “function” in place of “element”.

when we model real numbers in ZFC, we represent them as equivalent classes of sequences of rational numbers.

A couple of years ago I gave a seminar about this stuff at the University of Barcelona, and got an unexpectedly hot reception from some of the set theorists in attendance. This didn’t make for the easiest afternoon, but I’m glad it happened that way, because it taught me a lot about how to present this material without unnecessarily fanning flames.

One of the comments was from the set theorist Joan Bagaria (who, I hasten to add, was absolutely calm and polite). He helpfully pointed out that ZFC itself is simply an axiomatic system, and says nothing about how to encode mathematical objects as sets. I knew this perfectly well, but I’m sorry to say that in my talk I’d been sloppily using the term “ZFC” to encompass both things at once. (In my paper, I use terms like “the traditional approach to set theory” instead.)

So, “when we model real numbers in ZFC” doesn’t really make sense. There’s no modelling of anything going on in ZFC. I guess you really mean “when we model real numbers as sets”, but then ZFC hasn’t got a lot to do with it. For example, in ETCS (the axiomatization explained in my paper), real numbers are modelled in the same way.

As I guess you know, there are actually many ways of modelling real numbers as sets. The way you describe is one. Dedekind cuts are another (giving rise to a few specific options, depending on exactly what you take the definition of cut to be). There are others too.

at least it answers the question in your article.

I wouldn’t agree. You’ve taken a particular set $S_\pi$ encoding the real number $\pi$, and a particular set $S_{\mathbb{R}}$ encoding the set $\mathbb{R}$, and you’ve answered the question “what is $S_\pi \cap S_{\mathbb{R}}$?” This isn’t necessarily the same question as “what is $\pi \cap \mathbb{R}$?” That is, whether one regards those as the same questions reflects one’s opinions about foundations; I would say not.

It’s very kind of you to say so. Thanks.

I have a question: ETCS seems silent on how to treat collections of large size, e.g., the collection of all groups or the forgetful functor from groups to sets.

Yes, indeed.

Is there an axiomatic system that is like ETCS in spirit and handles universes?

Others here will do a better job of answering that than I could. In short, (i) people have certainly tried to create such a system, and (ii) there is a point of view that this isn’t the right thing to do. That point of view says that it would be better to axiomatize the category of categories (as opposed to classes, say). Lawvere proposed such an axiomatization (e.g. see this MathOverflow question); it had some mistakes that I think later got fixed. A variant of that viewpoint is that one should axiomatize the 2-category of categories instead (e.g. see Mike Shulman’s answer to that MO question).

On (i), one key phrase to look for is algebraic set theory. However, AST in general is analogous to general topos theory, and I don’t know whether anyone has distilled out of it a “well-pointed” axiomatic system analogous to ETCS. The situation with 2-topos theory is similar. On the other hand, I should also point out that ETCS (and topos theory in general) has no problem with universes.

In particular I am quite happy that next time I teach our “Introduction to proofs” course, I will not feel guilty about treating functions as primitives rather than as a set-theoretic constructs.

I haven’t read the draft yet, but this was one of my main reactions to the post.

L’Enseignement Mathématique

Do you think the tone is right for l’Enseignement? I’m not familiar with many papers in there, but those I’ve seen are written in a style rather more formal and less journalistic than that of my own paper. I see you’ve got a couple of papers in l’Enseignement yourself, so you’re probably a good person to ask.

Does anyone think American Mathematical Monthly is a good idea? Would my article fit? It’s hard to see what the articles they publish are like, as they don’t seem to be available except to subscribers.

By the way, there’s an excellent list of journals publishing expository work at MathOverflow. (Well, it’s excellent in the sense that it’s probably quite comprehensive, but it’s perhaps disheartening how sparse the field is.)

What I really want to know is whether there are any journals where my article’s likely to fit, in terms of level, style, length etc.

Hi!

Hi!

I do not understand why you put the “reactions to an earthquake”-section into the article. I do not see any objection in this section which distinguishes classical set theory from categorical set theory.

The point was that people’s reaction to the discovery of an inconsistency in a list of set-theoretic axioms is illuminating: it tells us something about how much they think their work actually depends on those axioms. It’s informative even as a thought experiment.

Suppose I make up a new set theory that has no connection with how anyone actually uses sets, then I discover an inconsistency in it. No one will care.

Now suppose I make up a new set theory consisting entirely of statements that mathematicians of all types use routinely, then discover an inconsistency in it. Everyone will care.

I argued at the beginning of the article that in certain respects, ZFC fails to reflect how non-set-theorists actually use sets — indeed, not only fails to reflect it but actively conflicts with it. This is why, I believe, most mathematicians wouldn’t feel that threatened if an inconsistency were found. (To be clear, I don’t claim ZFC has no connection with how anyone uses sets, just that it’s further from reflecting ordinary usage than is generally appreciated.)

On the other hand, every axiom of ETCS is a statement about sets that everyone believes makes sense. They are all principles used by mathematicians all the time. Were any one to fail, it would cause the most enormous upheaval.

As I said in the last paragraph of my paper, the question of strength is peripheral. Let’s say we adjust ETCS and/or ZFC so that the proof-theoretic strengths match exactly, in one of the ways described. An inconsistency can be found in one iff it can be found in the other.

Still, people can feel differently about an inconsistency in one versus an inconsistency in the other. I think that if ETCS was more widely known, people would be way more shocked by an inconsistency in it than an inconsistency in the equivalent fragment of ZFC, simply because the usage of “set” in ZFC is so different from how most people use it.

Hi,

But in the SGA universes are used, weren’t they introduced especially for SGA?

yes, they were used, but apparently not necessary. McLarty shows that derived functor cohomology only requires a reasonably weak set theory, and for concrete applications (including using etale cohomology) even only third order arithmetic or so is needed (plus the assumption of some standard uncountable ring like the complex numbers). I gather that this is the only (or at most, one of very few) place(s) in SGA where universes were really necessary. There is some discussion by knowledgeable experts at this MO question.

Sylvain, as Tom pointed out in his original post, it’s easy for these kinds of discussions to be heated, so it’s important to be extra-extra-polite. (I’ve been as guilty of violating this as anyone.)

In some ways, phrasing topics in terms of foundations detract from the mathematical content of them. For example, ETCS shows that there a first-order theory of “sets identified only up to isomorphism” that is equivalent to bounded Zermelo with choice set theory, and therefore can prove most results in mathematics. That means that you could rewrite those proofs into proofs entirely in the logic of “sets up to isomorphism” and functions between them. I would rather be set on fire than write out such a proof, but that is a perfectly interesting mathematical result, one that illustrates the extent to which mathematical results are invariant up to arbitrary choices of labeling. You could probably even state this as a precise theorem: if you have a theorem of bounded Zermelo with choice that does not mention elements, then it has a proof that does not mention elements.

Footnote: I wrote

Since we’re in a topos

That was a slightly cheaty thing to say. A category satisfying the axioms in my paper is indeed a topos, but that’s not instantly obvious. There are two wrinkles: (i) instead of requiring the existence of finite products and equalizers, I require the existence of finite products and fibres over elements; (ii) instead of requiring the existence of a set $2$ classifying monos (i.e. a subobject classifier), I require the existence of a set $2$ classifying injections. Given that, you might imagine that well-pointedness would be needed in order to prove it’s a topos.

Nevertheless, I checked the details and it all works out: from the axioms as I stated them, one can construct equalizers without using well-pointedness.