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.

 

Advertisements

About fwaaldijk

mathematician (foundations & topology in constructive mathematics) and visual artist
This entry was posted in Uncategorized. Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s