What does category theory say about chains of set inclusions $\dots\in c\in b\in a$?

Question

I'm currently trying to understand to what extent a set theory like ZFC can be mirrored within category theory, i.e. topos theory.

What appears as an obstacle to me is the axiom of regularity, which solves some paradoxical foundational questions and the related well-foundedness concepts: In a category theoretical set theory, e.g. ETCS, the point is to avoid a membership predicate "$\in$" and nestings of sets like $b\in a,\ c\in b,\ d\in c,\dots$. Subobjects are characterized via arrows and the "regular" topoi which are like set theories characterize elements as single injections too.

Does category theory let us formulate any statement which relates to regularity?

Naively it would appear that the theory doesn't leave us any choice but exclude the phenomenon which the classical formulations axiomize away. But then to what extend does the theory leave you a choice and to what extend can you deviate from it?

Appearently non-well-foundedness is a thing now. (And I even read somewhere on MathOverflow that the proof of the abc-conjecture relates to it.) And so I assume you can speak about it in category theory as well.

Answer 1

Topos theory yields a wholeheartedly structural set theory — the question is not a meaningful one, since objects having 'elements' is a matter of convention rather than being any intrinsic part of the identity of the object.

Furthermore, unlike type theory where each each type comes with a canonical interpretation (and we can talk about well-founded types), topos theory doesn't even have that: category theory only cares about the identity of objects up to isomorphism.

To wit, while ZFC would carefully distinguish between two terminal sets $\{ \varnothing \}$ and $\{ \{ \varnothing \}\}$, the point of view from category theory is that they are isomorphic objects, and thus interchangeable (by transport along isomorphisms) for all purposes.

Thus, we can arrange for a descending chain of element inclusions where the unique element of a one-point set

More generally, any set $S$ represents a canonical subobject of $\mathcal{P}(S)$: specifically the subobject given by the "singleton set" function $S \to \mathcal{P}(S)$.

For a more interesting example, consider the function $f : \mathbb{Z} \to \mathcal{P}(\mathbb{Z})$ given by

$$ f(x) = \{ y \in \mathbb{Z} \mid y \leq x \} $$

$f$ is monic, and thus identifies $\mathbb{Z}$ with a subobject of $\mathcal{P}(\mathbb{Z})$. Thus, the binary relation $\in$ defined by its graph in $\mathbb{Z} \times \mathcal{P}(\mathbb{Z})$ restricts to a relation on $\mathbb{Z} \times \mathbb{Z}$ (in fact, precisely the relation $\leq$), and thus we have lots of nontrivial membership chains.