How would set theory research be affected by using ETCS instead of ZFC? In "Rethinking Set Theory", Tom Leinster argues in favor of teaching axiomatic set theory via Lawvere's Elementary Theory of the Category of Sets with 10 axioms (but phrased in a way that requires no knowledge of category theory) which uses sets and functions as primitive elements compared to ZFC which uses sets and elements as primitives. (although if you really insist you can reintroduce elements as primitives at the expense of more clauses). This is weaker than ZFC but can be made equivalent to ZFC (or equiconsistent according to François G. Dorais) with the addition of a hardly ever needed 11th axiom.
http://golem.ph.utexas.edu/category/2012/12/rethinking_set_theory.html
How would set theory research be affected by using ETCS instead of ZFC?
Is ETCS less cumbersome than ZFC or more, or does it not matter? Does it make proofs longer/shorter or easier/harder?
Would automated theorem provers work better with ETCS?
To clarify, the question is not about the strength of ETCS: assume whatever is needed to bring ETCS up to strength with ZFC. The question is about practicalities of working with the ETCS axioms. I guess most mathematicians don't directly work with axioms of set-theory at all. So the question is: if your work does involve working directly with such axioms then what difference (if any) does it practically make to you as a set-theory researcher to use a different set of axioms that have equal strength. If I understand correctly the goal of Tom Leinster's paper was to reflect actual (non-set-theoretical)-mathematical practice but my question is about what set-theorists would do if they used these axioms. Assume also that for the purposes of this question ETCS refers specifically to the rephrasing used in this paper that is free of category and topos terminology. Perhaps this rephrasing should be renamed ETS. Adding replacement would give the name ETSR.
 A: Some quotes:
"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’."
, John Baez http://golem.ph.utexas.edu/category/2012/12/rethinking_set_theory.html#c042716
"There are some problems with this sort of compromise where material and structural set theories cohabitate as equal alternative foundations. ... this kind of cohabitation model is actually not the best possible way to accommodate both the material and the structural perspective at the foundational level. ... what we end up doing is moving all the annoyances from both sides into the translation between the two ...  it would be much more satisfactory to have a greater overarching foundation similar to Cantor’s universe that comprises both the material and structural views.", François G. Dorais http://dorais.org/archives/1135
"if you care about internalizing mathematics in nonstandard models — not only in order to prove formal independence results, as set theorists do, but because you care about the nonstandard models in their own right and you want to use internalization to prove things about them — then ETCS is your friend and ZFC is your enemy.  Structural set theory — and its sister, type theory — is very well adapted to internalizing in many different contexts"
, Mike Shulman http://golem.ph.utexas.edu/category/2012/12/rethinking_set_theory.html#c042933
"with ZFC is that it allows things like ⟨0,1⟩⊆3 which make no sense mathematically. I can assure you, though, that after you write one piece of code in x86 assembler which rewrites itself as it runs that manipulating all objects as binary and manipulating all objects as sets make perfect sense. This is what annoys me, in some sense, that people have an issue that in a system which allows you to encode everything as sets you can write some weird junk. Equivalently, this would be baffling to those people that if you write a piece of code in Common Lisp then the code itself is just a list and the program can manipulate itself (easier than to do that in assembler, I have to admit).", Asaf Karagila
http://karagila.org/2013/on-leinsters-rethinking-set-theory/#273
"I don’t like the hard line that certain things are meaningless, simply because this depends on the setting.  I don’t object to the idea of saying that an expression is, for your current purposes, well-typed, since this just means you say nothing about non-well-typed expressions.  I would say not “meaningless”, but rather “does not have an intended meaning”.  There are expressions, such as 0∈1 that do not have an intended meaning.  If they have a meaning in a certain setting, then so be it.", Walt http://golem.ph.utexas.edu/category/2012/12/rethinking_set_theory.html#c042992
"ETCS is one, but apparently not one that is very congenial to many traditional set theorists, for a variety of reasons, maybe one being that many set theorists “don’t like categories” (well, okay, but again I think that’s a pity). Maybe some set theorists don’t like the privileging of functions over elements (although one take is that functions are generalized elements).", Todd Trimble, 
http://karagila.org/2013/on-leinsters-rethinking-set-theory/#277
"The same arrows aimed at ZFC can be easily turned at ETCS. It is equally easy to ask about “senseless things” which happen in ETCS but not in general mathematics. And this is not a critique against ETCS, but rather against the critique aimed at ZFC.", Asaf Karagila http://karagila.org/2013/on-leinsters-rethinking-set-theory/#289
"the issue is that first-order logic is not “type safe”, and I would suspect that people who have had exposure to first-order logic take this for granted, while those who have not may find it surprising. The reason is that syntax, in first-order logic, is defined independently of semantics, so that whether a formula is well-formed (syntactically correct) is independent of what the formula means. ... This issue of “type safety” arises also in programming languages. Some languages, such as C, have little run-time type checking. I can take a 64 bit integer and treat it as an array of eight 8-bit characters – with implementation-defined results. ... In working mathematics we have humans to check that the formulas we actually write make sense – nobody accidentally writes 1∈sin in an analysis paper – so it is not clear that there is any real advantage to stronger “type checking” in the foundations.", Carl Mummert http://karagila.org/2013/on-leinsters-rethinking-set-theory/#274
A: No one has really addressed the question about automated theorem provers.  I'm going to take this to refer more generally to computer-assisted mathematics, since fully automated theorem provers are still of very limited usefulness to a mathematician.  There are a lot of good arguments that the best foundational system for these is neither ZFC (or its relatives) nor ETCS (or its relatives), but some variety of type theory.
This is mainly because type theory is so closely connected with programming and has good computation behavior, thus meshing very well with computers.  Since the question is not about type theory, I won't say much about it; I just want to point out that ETCS is more like type theory than ZFC is.  So although I kind of doubt that actually using ETCS in a computer proof assistant would be much better than using ZFC, learning to think in ETCS and do mathematics therein will probably stand you in better stead when you try to use a proof assistant based on type theory.
A: There are several relatives (typically: subtheories and supertheories)  of ZFC that are used in set-theoretic research.  If somebody wants to do set theory based on ETCS or a related base theory, these theories would have to be translated to this new base (or, in the case of theories that are not so canonical, such as ZFC*, substitutes would have to be found).  
Such a translation seems to be rather straightforward in the case of supertheories; a good translation would of course use the idioms of the target language. 


*

*Examples of supertheories:

*

*ZFC plus large cardinals

*ZFC plus definable determinacy (e.g., projective determinacy, or some consequences thereof - related to large cardinals). 

*ZF plus AD, or ZF + $V=L(\mathbb R)$ (supertheory of ZF only)

*ZF(C) plus "V is a certain inner model".  Weaker versions include:

*

*ZFC plus cardinal arithmetic assumptions (GCH, SCH)

*ZFC plus combinatorial principles ($\diamondsuit$, etc)


*ZFC plus forcing axioms (MA, PFA etc)

*others, including combinations (conjunctions) of the above


*Examples of subtheories

*

*KP and related theories, which do not have full comprehension. (I think they are usually associated with proof theory rather than set theory)

*ZFC minus infinity (this is more closely associated with arithmetic than with set theory)

*ZF, or ZF plus weak versions of choice

*ZFC minus power set (plus instances of power set).  Typical models are of the form $H(\chi)$. 

*ZFC minus replacement (plus finitely many instance of replacement). Typical models are $V_\delta$. 

*ZFC*, an often unspecified finite subset of ZFC, used to get around the "undefinability of truth", or to apply the reflection theorem.  (Morally the same as the previous item.) 

*ZFC minus Foundation, reflecting the fact that Foundation is hardly used outside set theory. 

*Others, including combinations (intersections) of the above


*Other relatives: 

*

*ZF(C) with atoms, perhaps closer to mathematical practice than ZFC itself. 

*NBG.  The relation between NBG and ZFC is very well understood, as are the advantages and disadvantages: On the plus side, NBG can naturally talk about classes, and is finitely axiomatized (which might make it more amenable to automated theorem proving). On the other hand, the fact that not every subclass of $\mathbb N$ is a set can be inconvenient. 

*MK and others. 

*NF and NFU, sometimes claimed to be more natural than ZFC.  While ZFC makes it awkward to talk about classes, NFU has problems with the function $x\mapsto \{x\}$. 


A: Well, one would just add a just strong enough instance of replacement, or the consequence one actually needs, to the assumptions of the theorem one was proving. For instance, one could take the existence of $\aleph_\omega$ as an assumption (like a large cardinal) rather than proving it exists. There are models of ETCS in which this exists and in which it doesn't. In this instance, one is just lowering the level at which one considers a cardinal 'large'.
I'm reminded of McLarty's recent work on weak set theories, and doing algebraic geometry in them. One can prove strong results about cohomology, but can't prove the existence of an uncountable ring like $\mathbb{R}$ or $\mathbb{C}$. He says you can just simply posit the existence of such a thing on top of the weak set theory, and then all the theorems go through.
Of course, in set theory there are a whole stack of results that rely on the strength of ZFC beyond ETCS, and it would entail a whole lot of reverse mathematical effort to find out what is actually necessary for swathes of theory, that many would say it is easier to just assume what ZFC gives you. But it isn't strictly necessary, just a lot easier.
A: I like the fact that you asked this question, but I'm a little worried that it will be seen as "subjective and argumentative".
For the second question, I think a lot of set theorists (trained since childhood in ZFC) have gone on record saying they do find ETCS not easy to work with or not user-friendly, and I find this quite understandable. There is a critical hump of lemmas to get over in the beginning when working with ETCS, because unlike ZFC or some variation thereof, there is no ready-made comprehension scheme in ETCS (at least as it is ordinarily presented). Rather, a stock of instances of comprehension (where one builds up an "internal logic" by hand, as it were) have to proven before one is ready to fly. But after some point, with enough of these beginning lemmas under the belt, the development of mathematics, say of the core undergraduate curriculum involving basic results of real analysis, algebra, topology, etc., proceeds pretty much the same way as what one is used to. So in that sense, I'd say "it does not matter" for the needs of working mathematicians.
In developing his new set theory SEAR (Sets, Elements, And Relations), Mike Shulman recognized this cumbersome aspect of ETCS, quoting an analogy I made once about ETCS on the now-moribund "Todd and Vishal's blog":

[Trimble] "with ZFC it’s more as if you can just hop in the car and go; with ETCS you build the car engine from smaller parts with your bare hands, but in the process you become an expert mechanic, and are not so rigidly attached to a particular make and model."
[Shulman] Using this metaphor, SEAR can be thought of as an ETCS-car which comes preassembled with a nice slick control panel. Or, using an alternate metaphor, ZFC is like Windows, ETCS is like UNIX, and SEAR is like OS X (or maybe Ubuntu). With SEAR you get a nice familiar interface with which it is easy to do standard things, there is less cruft than you get with ZFC, and behind the scenes you have all the power of ETCS (and more). (Of course, if you like Microsoft products, then this metaphor probably does not appeal to you.)

So SEAR aims to combine the advantages of ETCS (as a truly "structural" set theory, where the aspects of sets we truly care about are isomorphism-invariant, and carry less "cruft") with the advantages of ZFC (where comprehension principles, etc. are built right in; see his axiom 1). SEAR will probably look more home-y and familiar to those used to traditional naive set theory; there is none of this intimidating "well-pointed topos with NNO and choice" business to wade through at the outset.
A: In principle, nothing would be lost by working in ETCS+R instead of ZFC since the two theories are very nicely interpretable in each other. However, after talking it through with Mike Shulman (whom I thank very much) here, I came to the conclusion that much would be lost in practice.
The problem lies with the notion of wellfoundedness. Recall that a binary relation $R$ on a set $A$ is wellfounded if every nonempty subset $B$ of $A$ has an $R$-minimal element (an $x \in B$ such that $y \not\mathrel{R} x$ for all $y \in B$); this is a $\Pi_1$ statement in the Lévy hierarchy. In ZFC, an equivalent statement is that there is an ordinal valued rank function for $R$ on $A$ (a function $r:A \to \mathrm{Ord}$ such that $x \mathrel{R} y \Rightarrow f(x) \lt f(y)$ for all $x,y\in A$). This is a $\Sigma_1$ statement in the Lévy hierarchy due to the fact that being an ordinal is $\Delta_0$. In ETCS+R, there is no suitable equivalent to ordinals: two wellorderings of the same type are indistinguishable from each other. Because of this, in ETCS+R, the equivalent rank function statement is much more complex since one must explicitly say that the codomain of the rank function is a wellordering (for which we must use the $\Pi_1$ definition).
Since wellfoundedness is $\Delta_1$ in ZFC, it is absolute for transitive models (of a small fragment) of ZFC. In other words, transitive embeddings between models of ZFC preserve wellfoundedness. (An embedding $f:M \to N$ is transitive if $f$ maps the elements of $x$ in $M$ onto the elements of $f(x)$ in $N$ for every $x \in M$; so the range of $f$ is a transitive substructure of $N$ isomorphic to $M$.) For models of ETCS+R, there is no natural equivalent to transitive embeddings so if one wants to preserve wellfoundedness then one must explicitly require that. In practice, it is very difficult to check that an embedding preserves wellfoundedness, especially when compared to checking that an embedding is transitive.
Therefore, ETCS+R does not have a very good grasp of wellfoundedness compared to ZFC. Since the study of wellfoundedness is so central to modern set theory, the framework of ZFC is much more appropriate than ETCS+R for set theorists to work with. To rephrase an analogy I used elsewhere, asking a set theorist to work in ETCS+R instead of ZFC is like asking a ring theorist to work with ternary relations $A(x,y,z)$ for addition $x+y = z$ and $M(x,y,z)$ for multiplication $x \cdot y = z$: it's essentially the same, in principle, but it's simply not the right thing to do!
A: Much of set theory research (for example, a paper I'm currently working on, concerning certain ultrafilters over the natural numbers) would work just fine in ETCS.  But much of set theory research uses the axiom of replacement in ways that cannot be imitated in ETCS.  Tom Leinster's paper gives the example of the existence of the union of $\mathbb N$, its power set $\mathcal P(\mathbb N)$, the power set of that, and so on, iterated for countably many steps. To put it another way, ETCS cannot prove that there is a cardinal number $\kappa$ with infinitely many infinite cardinals below it.  Such $\kappa$'s and far larger ones are certainly involved in a great deal of research-level set theory, so a foundation having the strength of ZFC (or even more) is needed there.
