What is continuity, constructively?
The concept of continuity for mappings between metric spaces should coincide with that of uniform continuity in the case of a compact domain, and still give rise to a category. In Bishop's constructive mathematics both requests can be fulfilled simultaneously, but then the reciprocal function has to be abandoned as a continuous function unless one adopts the fan theorem. This perhaps little satisfying situation could be avoided by moving to a point-free setting, such as formal topology, in which infinite coverings are defined mainly inductively. The purpose of this paper is to discuss the earlier situation and some recent developments.
continuity constructive mathematics