Andrej Bauer isn't so sure about the conjecture: "we would have to know something useful about an arbitrary bijection [0,1] → (0,1), other than it not being continuous. For instance, if we knew it had a jump, we'd be done. How would one prove classically that such a bijection must have a jump? (As opposed to other kinds of discontinuities, where it just oscillates.)" ( https://mathstodon.xyz/@andrejbauer/112597232675231982 ) and if there has been further work on this I didn't notice it.
One direction of a conjecture by Martin Escardo on Mastodon is, to use iset.mm notation,
( 0 [,] 1 ) ~~ ( 0 (,) 1 ) -> _om e. WOmni.The other direction is a separate issue: https://github.com/metamath/set.mm/issues/4067
Andrej Bauer isn't so sure about the conjecture: "we would have to know something useful about an arbitrary bijection [0,1] → (0,1), other than it not being continuous. For instance, if we knew it had a jump, we'd be done. How would one prove classically that such a bijection must have a jump? (As opposed to other kinds of discontinuities, where it just oscillates.)" ( https://mathstodon.xyz/@andrejbauer/112597232675231982 ) and if there has been further work on this I didn't notice it.