Addendum to Natural Topology regarding functions

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 $f$ from an apartness space $(V,\#_1)$ to another apartness space $(W,\#_2)$ as a  subset of the cartesian product $V\times W$ such that:

i) for all $x\in V$ there is a $y\in W$ such that $(x,y)\in f$

ii) for all $x,v\in V, y,z\in W$: if $(x,y)\in f$ and $(v,z)\in f$ and $y \#_2 z$ then $x \#_1 v$.

Then for any pair $(x,y)\in f$ we write: $f(x)\equiv y$ or $f(x)=y$.

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.