[FOM] constructive continuity 2

[spitters]

On Friday 15 February 2008 19:49:38 hendrik at topoi.pooq.com wrote:
> The fact that [0, 1] is a closed interval, whereas R is like an open
> interval (0, 1) is surely relevant.
>
> What, by the way, *is* {[0, 1]}  It seems that the formal intervals and
> neighbourhoods are joins of open intervals; wherefor they'd correspond
> to open sets in R.  [0, 1] is not open.

In formal topology/locale theory [0,1] is defined as the formal complement of 
(-oo,0) cup (1,oo). This is a place where formal topology and Bishop's 
constructive mathematics differ. Bishop focuses on closed sets as the 
complete ones. These correspond (roughly) to formal closed in the sense of 
Sambin and weakly closed and open in terms of locale theory.

Some discussion of these issues is in our preprint:
http://arxiv.org/pdf/math/0703561

[We are currently revising this paper.]

Bas