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

395 Views Asked by At

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.

2

There are 2 best solutions below

0
On

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.

4
On

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).