Hello !

The Urysohn's Lemma assert that in every topological spaces which is normal two closed subset may be separated by a real valued function. It's proof use axiom of countable choice (but not the law of excluded middle).

I would like to find a counterexample to this theorem in the internal logic of a topos in which the axiom of countable choice does not hold (for exemple, the topos of smooth action of some non discrete locally pro-finite group, or the topos of sheaf on [0,1].)

I need a counterexample which is compact, but If you have an example involving not a topological space but a local (an example of compact regular local which does not have enough functions with value in the Dedekind real) it's perfectly fine for me.

Thank you !

Consequences of the Axiom of Choiceconsequences.emich.edu/conseq.htm It is known to be false in the models $\mathcal{N}3$ and $\mathcal{N}8$; these are two permutation models. (I think the first is one of the original Mostowski models and the other is due to Laüchli, but I don't have the book handy right now.) – François G. Dorais♦ Apr 26 '12 at 15:26