I can't find a statement about the axiom of regularity anywhere in treatments of ETCS. Perhaps this is due to the unfortunate clash of terminology with 'foundations'.

3$\begingroup$ This should be relevant. $\endgroup$ – Michael Greinecker Jan 8 at 18:09

$\begingroup$ I suspect that ETCS is not wellfounded in any reasonable sense. One particular way to phrase this might be the following: there are illfounded models of ZFC  Foundation + $\neg$Foundation which "translate" in the appropriate sense to models of ETCS. $\endgroup$ – Noah Schweber Jan 8 at 18:16

1$\begingroup$ At the same time, it's not entirely clear to me what "foundation" would mean in the context of ETCS (where we're not basing everything on elementhood after all). In fact, I'd guess the following: if $M$ is a model of ETCS "generated" by a wellfounded model $N$ of ZFC, there is a model of ZFC  Foundation + AFA which "generates" an isomorphic model. (Besides the obvious vagueness, I'm being a bit rude here in my mix of classical modeltheoretic language and ETCS, but I think this is benign in this context.) $\endgroup$ – Noah Schweber Jan 8 at 18:19

$\begingroup$ @NoahSchweber this is my gut feeling too. The more I look into this problem the more it becomes clear that ETCS is quite different of a beast from ZFC (at least modelwise). The question of wellfoundedness then makes little sense, from a certain point of view. On the other hand, it is natural to ask how are the two theories related: in which sense ETCS sets are ZFC sets? $\endgroup$ – mattecapu Jan 8 at 18:26

1$\begingroup$ Does the pope poop in the woods? $\endgroup$ – Asaf Karagila Jan 8 at 18:51
As Noah suggests, the axiom of regularity doesn't make sense in the language of ETCS. What we can say is:
 To construct a model of ETCS+R from a model of ZFC, one doesn't need regularity.
 From a model of ETCS+R, one can construct a model of ZFC with regularity, and also separately models of ZFC with regularity replaced by various antifoundation axioms.
The composite ETCS+R > ZFC > ETCS+R is the identity, as are the illfounded versions. And the composite ZFC > ETCS+R > ZFC is also the identity, as are illfounded versions whose antifoundation axiom is sufficiently strong to characterize possible setmembership diagrams structurally.
Among other places, more details can be found in this paper of mine.

3

$\begingroup$ @NoahSchweber Yes, R denotes any of the equivalent replacement/collection axiom schemas that can be added to ETCS. $\endgroup$ – Mike Shulman Jan 9 at 21:28

$\begingroup$ Is there a “canonical” way of interpreting ZFC in ETCS, about which one may ask whether one ends up with a wellfounded model? $\endgroup$ – Monroe Eskew Jan 11 at 11:28

1$\begingroup$ @MonroeEskew Since "ZFC" by definition includes the regularity axiom, I would argue that the construction of a model with regularity is the canonical way of interpreting ZFC in ETCS. And there's similarly a canonical way of interpreting ZFCregularity+AFA in ETCS. But no, there's no way of constructing such an interpretation without deciding in advance whether you want it to satisfy regularity or not, and it'll basically always be possible to do both  ETCS doesn't "know" anything about regularity. $\endgroup$ – Mike Shulman Jan 11 at 20:23

$\begingroup$ Another way to think about it is that ZFC and ZFCregularity+AFA (AFA = antifoundation axiom) are essentially equivalent  one can construct a model of either one from the other  and passing back and forth between them doesn't change the corresponding model of ETCS. $\endgroup$ – Mike Shulman Jan 11 at 20:24