Define negation and disequality about book

[andrejbauer]

When we come to reals we shall see that there is something called "apartness" which is a strong form on disequality. Should we have a forward reference to that in Ch 1? (Probably not.)

[mikeshulman]

Probably not in Ch 1, but it might make sense in, say, 2.8.3 to mention generally that sometimes a concept that's defined classically using negation may have a constructive version defined without using negation.

[andrejbauer]

Ok, I am assigning tihis issue to myself so I remember to come back to 2.8.3. I will close the issue when I am done.

[EgbertRijke]

But it shouldn't be called a constructive version of negation (there's nothing non-constructive about negating).

[mikeshulman]

Maybe 'positive' is a better word for what I meant? I mean something that
you prove by doing something, rather than by showning that you can't do
something.
On Mar 25, 2013 3:49 PM, "EgbertRijke" [email protected] wrote:

But it shouldn't be called a constructive version of negation (there's
nothing non-constructive about negating).

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/19#issuecomment-15419402
.

[andrejbauer]

I did something, please check. It seems hard to find a good spot for the definition of negation.