On a continuity theorem for constructive functions (Q2253862)

The paper aims at characterising the class of uniformly continuous maps of compact constructive metric spaces without using the notion of continuity, and not presuming the functions can be extended to formal points. Specifically, the major result in the paper is the proof that a total constructive map from a compact metric space into a complete metric space preserving the precompactness of subsets, is uniformly continuous. Although the paper is very neat and clear, it may pose a number of difficulties to a potential reader. In the first place, it refers to Shanin's and Markov's view of constructive mathematics, which differs in many aspects to other approaches. In particular, in the context of the paper, it is worth reminding that Markov accepts a variant of Church's thesis, while Bishop does not use it, even if accepting it as plausible. Also, in the Russian constructive approach to mathematics, the so-called Markov's principle, stating that \(\neg \neg \exists x.\, A\) entails \(\exists x.\, A\) is assumed, provided \(A\) being decidable, while the principle is rejected in the other major systems, especially Brouwer's and Bishop's. A good starting point to understand the conceptual framework of the article is [\textit{B. A. Kushner}, Am. Math. Mon. 113, No. 6, 559--566 (2006; Zbl 1110.01009)]. The second major difficulty is that most background results, cited in the first part of the work, have been published in the sixties and the seventies in USSR journals, and they are in Russian. Not all of them are easily accessible, and some of them have not been translated. The dry style, emphasised by the numbering of paragraphs is very distant from the usual scholar standards: this way of presenting the content, which is typical of some parts of the Russian scientific tradition, may be intimidating, but, in fact, it helps to proceed along the proofs, by condensing each major step in a paragraph. The result is significant in the context of Markov's constructive mathematics, but to fully appreciate, it is worth comparing the similar achievements in Bishop's line of thought. In this respect, there are many references, for example, [\textit{D. Bridges} et al., Lect. Notes Comput. Sci. 2471, 89--102 (2002; Zbl 1021.03056)] provides a reasonably close starting point.