On Eq, was Re: [Haskell-cafe] When to use fancy types [Re: NumberTheory library]

[Peter G. Hancock]

>>>>> Lennart Augustsson wrote (on Sat, 14 May 2005 at 16:01):

    > Why would a constructivist think that all functions are continuous?
    > It makes no sense.

How would you define a non-continuous function (on reals, say)
without (something like) definition by undecidable cases? 

Formal systems for constructive mathematics usually have
models in which all functions |R -> |R are continuous. 

For a long time, constructive mathematics lacked an analogue of
classical point-set topology. (Bishop et al dealt mainly with metric
spaces.)  Nowadays, this seems to have been (crudely speaking)
"fixed".  Basically, one starts with the structure of neighbourhoods
(inclusion and covering), and analyses notions like point and
continuous function in those terms.  Some of the major contributions
to the subject have been made by people working in Sweden, at least
one in your own department. 

Peter Hancock