# Where is the well-pointedness assumption of ETCS used in everyday math?

Where is the well-pointedeness assumption of the Elementary theory of the category of sets (Lawvere's category-theoretic axiomatization of set theory) used in everyday math?

Specifically, if you have a topos with natural numbers object (assume choice if you want to), what familiar theorems don't hold? I've heard that showing the Dedekind reals are the same as the Cauchy reals is one. Where in the arguments is well-pointedness used? It seems hard to find examples of this.

-
what is "ETCS"? – T.. Nov 15 '10 at 20:43
Elementary theory of the category of sets. Lawvere's category-theoretic axiomatization of set theory. Well-pointed topos with choice and natural numbers object. – Ibrahim Tencer Nov 15 '10 at 21:10
Please try to make the body of your posts self-contained, not relying on the subject line for content. I've edited the question, also taking into account your response above. – Arturo Magidin Feb 14 '11 at 3:21

A topos with an NNO has intuitionistic internal logic in general (if you assume Choice then Dionescu's theorem tells you that the internal logic is classical), so any proof that relies on proof by contradiction will not work (not to say the results won't, but the proof needs to be fixed, or your concepts altered).

-
ok, but what if you assume Choice? – Ibrahim Tencer Sep 16 '11 at 20:49
A topos with NNO and Choice but not well-pointed would require arguments with generalised elements. I'm not aware off the top of my head of anything that would break ordinary mathematics. – David Roberts Sep 23 '11 at 2:49
Note that from the point of view of the internal language, any topos looks like it were well-pointed. Well-pointedness is an external property. Mike Shulman's beautiful stack semantics paper might be of some interest. – Ingo Blechschmidt Mar 10 '14 at 10:34
I should say 'Internal Choice' in my previous comment, as that is the only thing that makes sense without well-pointedness. – David Roberts Mar 11 '14 at 2:00

Ah, I forgot about the Yoneda lemma.

Also, I think it's impossible to show that a strictly increasing function into a partial order is monic, because the normal proof uses the fact that monic on global elements implies monic. In fact, this lemma is probably used a lot.

-