Constructive uniformities of pseudometrics and Bishop topologies

Abstract

We develop the first steps of a constructive theory of uniformities given by pseudometrics and study its relation to the constructive theory of Bishop topologies. Both these concepts are constructive, function-theoretic alternatives to the notion of a topology of open sets. After motivating the constructive study of uniformities of pseudometrics we present their basic theory and we prove a Stone-Cech theorem for them. We introduce the f-uniform spaces and we prove a Tychonoff embedding theorem for them. We study the uniformity of pseudometrics generated by some Bishop topology and the pseudo-compact Bishop topology generated by some uniformity of pseudometrics. Defining the large uniformity on reals we prove a ``large'' version of the Tychonoff embedding theorem for f-uniform spaces and we show that the notion of morphism between uniform spaces captures Bishop continuity. We work within Bishop's informal system of constructive mathematics BISH extended with inductive definitions with rules of countably many premisses.