Definition and use of \ne (aka \neq)

[marcbezem]

In 2.12.1 we define $a\ne b$ as the negation of $a \eqto b$. It is used four times in Ch. 2, and only when $a$ and $b$ are elements of a set. Two out of four times is used before the reader knows what a set is, and thus before we have defined $a = b$. The definition of $\ne$ would ideally be moved to after the definition of $a=b$ and restricted to sets.

1. Arguments for moving: it is more systematic, a little better.
2. Arguments for not moving: 2.12.1 would become more cumbersome, negated types are propositions anyway, it has so far not be used for other types than sets (which I think we shouldn't).

May I have your votes, please (I vote for 2)?

[UlrikBuchholtz]

I vote 2 as well.

[DanGrayson]

I vote 1.

[DanGrayson]

In line with this, and the recent changes in commit b16b4cfeb29b47d5af3922d0b8e1a270f6b6c1ff, we still define the negation of a type this way:

Do we really need it? Can we wait and define negation just for propositions? It is a logical operator, after all.

[UlrikBuchholtz]

Now resolved!