Original question: For compact metric spaces, plenty of subtly different definitions converge to the same concept. Overtness can be viewed a a property dual to compactness. So is there a similar story for overt metric spaces?

Edit: Since Overtness is trivially true assuming the Law of the Excluded Middle, clearly the question is primarily interesting when we do not assume the LEM.

Edit 2: It looks like it is extremely difficult for a metric space to not be overt even in constructive settings. So editing the question to ask if there is ANY model where metric spaces are not overt.