Skip to main content
2 of 5
added 40 characters in body

What is the status of Jordan's theorem in constructive mathematics in the language of locales?

By constructive mathematics in this matter we mean ZF without the law of the excluded third (*).

In the language of locales, the Jordan curve can be defined as $f\colon I \to X$ such that "if $U \cap V = \varnothing$, then $f(U) \cap f(V) = \varnothing$" (coincides with the classical definition for Hausdorff spaces).

So, is Jordan's theorem true for locales in constructive mathematics?

(*) I like Martin-Löf's intuitionistic theory of types more and it seems that in a sense "this is the same question", but I have not studied the type theory systematically yet, so I am formulating the question in a more familiar language.