In the appendix, I omitted to include the definition of `function´ in section A.4 Constructive concepts and axioms used. The reason is that we use the standard classical definition:
Having taken the notion of `set´ and `subset´ as primitive, we define a function from an apartness space to another apartness space as a subset of the cartesian product such that:
i) for all there is a such that
ii) for all : if and and then .
Then for any pair we write: or .
The constructive interpretation of the quantifiers `for all´ and `there is´ ensures in our eyes that this definition nicely captures the connotation of methodicity which the word `function´ carries. In the book we almost always work with morphisms anyway, but the definition above is strictly speaking necessary to underpin the theorems on representability of continuous functions by morphisms.