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

[karczma at info.unicaen.fr]

Jacques Carette writes: 

> Anyone who thinks that +0 = -0 has never wrestled with a branch cut (and 
> lost...).  Such people have the nasty habit of also thinking that ALL 
> functions are continuous!  You might think they were constructivists or 
> something.

HmHmHm...
Why do you think that constructivists are against +0 /= -0?
Or that they think that all functions are continuous?
Do you think that Per Martin-Löf would a priori reject -0 as
  a typed object ? 

There are some physicists which have some bias towards constructivism,
since for them the Mathematical Nature of the Nature is constructive, the
sense of the word 'exist' is *not* so abstract...
Yet, they know that physical quantum amplitudes *must* have branch cuts
because of unitarity... 

Yours, as always off-topically, 

Jerzy Karczmarczuk