An axiomatic development of the theory of apartness and nearness of a point and a set is introduced as a framework for constructive topology. Various notions of continuity of mappings between apartness spaces are compared; the constructive independence of one of the axioms from the others is demonstrated; and the product apartness structure is defined and analysed.

Uniform sequential continuity, a property classically equivalent to sequential continuity on compact sets, is shown, constructively, to be a consequence of strong continuity on a metric space. It is then shown that in the case of a separable metric space, uniform sequential continuity implies strong continuity if and only if one adopts a certain boundedness principle that, although valid in the classical, recursive and intuitionistic setting, is independent of Heyting arithmetic.

We extend the concept of apartness spaces to the concept of quasi-apartness spaces. We show that there is an adjunction between the category of quasi-apartness spaces and the category of neighbourhood spaces, which indicates that quasi-apartness is a more natural concept than apartness. We also show that there is an adjoint equivalence between the category of apartness spaces and the category of Grayson’s separated spaces.

The main purpose of this paper is to investigate constructively the relationship between proximal convergence, uniform sequential convergence and uniform convergence for sequences of mappings between apartness spaces. It is also shown that if the second space satisfies the Efremovic axiom, then proximal convergence preserves strong continuity.

In the constructive theory of uniform spaces there occurs a technique of proof in which the application of a weak form of the law of excluded middle is circumvented by purely analytic means. The essence of this proof-technique is extracted and then applied in several different situations.

The theory of apartness spaces, and their relation to topological spaces (in the point–set case) and uniform spaces (in the set–set case), is sketched. New notions of local decomposability and regularity are investigated, and the latter is used to produce an example of a classically metrisable apartness on R that cannot be induced constructively by a uniform structure.

The relation between near continuity and sequential continuity for mappings between metric spaces is explored constructively. It is also shown that the classical implications “near continuity implies sequential continuity” and “near continuity implies apart continuity” are essentially nonconstructive.

In the constructive theory of uniform spaces there occurs a technique of proof in which the application of a weak form of the law of excluded middle is circumvented by purely analytic means. The essence of this proof—technique is extracted and then applied in several different situations.

We investigate separation properties for neighbourhood spaces in some details within a framework of constructive mathematics, and define corresponding separation properties for quasi-apartness spaces. We also deal with separation properties for spaces with inequality.

A natural extension theorem for strongly continuous mappings, the morphisms in the category of apartness spaces, is proved constructively.

The paper deals with proximal convergence and Leader's theorem, in the constructive theory of uniform apartness spaces.