In categorical set theory, we observe that certain topoi satisfy (suitable versions of) certain axioms from set theory. For example, Lawvere's $\mathsf{ETCS}$ asserts that $\mathbf{Set}$ is a well-pointed topos with a natural numbers object, satisfying the (internal) axiom of choice. $\mathsf{ETCS}$ is known to be equivalent to $\mathsf{BZC}$, a fragment of $\mathsf{ZFC}$ which *doesn't* include regularity.


My question is: **what does it take for a topos to satisfy** (a suitably phrased version of) **the axiom of regularity?** Or perhaps some statement which is equivalent (in the presence of the other $\mathsf{ZFC}$ axioms), as I understand regularity is not intuitionistically acceptable.



When does a topos satisfy the axiom of regularity?
The relationship between toposes and set theories was studied comprehensively in



> 
> Steve Awodey, Carsten Butz, Alex Simpson, Thomas Streicher: [Relating first-order set theories, toposes and categories of classes](https://www.sciencedirect.com/science/article/pii/S0168007213000730).
> Annals of Pure and Applied Logic, Volume 165, Issue 2, February 2014, Pages 428-502
> 
> 
> 


Regularity is discussed under the name "well-foundedness". You can find a lot of details in the paper, I am just going to quickly review the setup.


We work in an elementary topos $\mathcal{E}$.


The first step is to cook up a notion of $\in$-membership.
Define a *membership graph* to be a triple $G = (|G|, A\_G, r\_G)$ where $|G|$ an $A\_G$ are objects and $r\_G : |G| \to A\_G + P|G|$ a morphism. We think of $|G|$ as a set of vertices with each vertex $x \in |G|$ being either an atom $a$ (in case $r(x) = \mathrm{inl}(a)$ for $a : A\_G$) or a branching vertex with adjacency set $d \subseteq |G|$ (in case $r(x) = \mathrm{inr}(d)$ for $d : P|G|$). We may define a bisimilarity relation $\sim\_{G,H}$ between two membership graphs expressing the fact that, up to reordering and repetition, $G$ and $H$ represent the same $\in$-membership structure. In other words, $\sim\_{G,H}$ expresses extensional equality of sets represented by $G$ and $H$. In particular, $\sim\_{G,G}$ is an equivalence relation which quotients the membership graph to give a membership relation that is extensional.


Next, we define a new topos $\mathcal{E}\_\mathrm{nwf}$ whose objects are triples $(D, m, G)$ where $G$ is a membership graph in $\mathcal{E}$, $D$ an object of $\mathcal{E}$, and $m : D \to |G|$ a mono in $\mathcal{E}$. A suitable notion of morphism is devised that takes into account the bisimilarity relations $\sim\_{G,H}$. We then have:


**Theorem 11.7:** *$\mathcal{E}\_\mathrm{nwf}$ is equivalent to $\mathcal{E}$.*


We may understand the theorem as saying that we enriched the topos $\mathcal{E}$ with membership relations to get $\mathcal{E}\_\mathrm{nwf}$, which changed the topos only up to equivalence (so not in any essential way from the point of view of topos theory).


So far we allow both atoms and non-well-founded membership relation. The next step is to define what it means for a membership graph $G = (|G|, A\_G, r\_G)$ to be well-founded. Here there are no surprises, as we can use the internal language of the topos to state when $X : P|G|$ satisfies the property "$X$ contains all the atoms $A\_G$ and is hereditarily closed under the membership relation $r\_G$" (see the formula after Corollary 11.2).


We define a third topos $\mathcal{E}\_\mathrm{wf}$ as the full subcategory of $\mathcal{E}\_\mathrm{nwf}$ of those objects whose membership graphs are well-founded.


**Proposition 11.3:** *The equivalence between $\mathcal{E}$ and $\mathcal{E}\_\mathrm{nwf}$ cuts down to an equivalence between $\mathcal{E}$ and $\mathcal{E}\_\mathrm{wf}$.*


The moral of the story is that, firstly, we may define a notion of extensional membership relation on objects in a topos, and secondly, that restricting to the well-founded part of the topos does not change the topos in a way that is relevant to topos theory.


In a sense the answer to the question "when does a topos satisfy the axiom of regularity" is "it does not matter". This is further discussed in the paper in Section 11.4, where the authors conclude with



> 
> *... it follows that any topos can be construed both as a model of BIZFA− and as a model of BINWFA−.*
> 
> 
> 


Here BIZFA- is their formulation of ZF-like set theory with foundation (regularity) and BIZWFA- a formulation of ZF-like set theory with anti-foundation.


Disclaimer: please do not take the above summary as a satisfactory description. The paper contains many more details and explanations, and it should be consulted for thorough understanding of the topic.


