Metric spaces in synthetic topology

We investigate the relationship between the synthetic approach to topology, in which every set is equipped with an intrinsic topology, and constructive theory of metric spaces. We relate the synthetic notion of compactness of Cantor space to Brouwer’s Fan Principle. We show that the intrinsic and metric topologies of complete separable metric spaces coincide if they do so for Baire space. In Russian Constructivism the match between synthetic and metric topology breaks down, as even a very simple complete totally bounded space fails to be compact, and its topology is strictly finer than the metric topology. In contrast, in Brouwer’s intuitionism synthetic and metric notions of topology and compactness agree.

► In synthetic topology every set is automatically equipped with intrinsic topology.
► We relate synthetic compactness with metric compactness and the Fan Theorem.
► We identify conditions under which intrinsic and metric topologies coincide.
► These conditions are satisfied in Type 2 Effectivity, but not in Type 1.