'Wrong' symbol for negated equality in Data.Rational.Unnormalised.*

[jamesmckinna]

The Base module introduces an ad hoc notation _≠_ for the negated equality in the setoid (ℚᵘ, _≃_) .
But there is now no reason to:

• the Unicode symbol _≄_ achieved via \~-n is (now available as) the 'correct' negation-correlated version of _≃_/\~-
• issues Add _≮_ and _≰_ to bundles in the binary relation hierarchy. #1214 and Relation.Binary.Bundles.Preorder declares the 'wrong' symbol for the ordering relation!!! #2096 and their associated PRs [fixes #1214] Add negated ordering relation symbols systematically to Relation.Binary.* #2095 Relation.Binary.Bundles.Preorder declares the 'wrong' symbol for the ordering relation!!! #2096 Add _≥_, _>_, _≱_ and _≯_ systematically to the Relation.Binary.Bundles hierarchy #2098 are aimed at rationalising the notation systems for all the negated/transposed equality/ordering symbols, so there's no need for an anomaly like this to persist.

[MatthewDaggitt]

So you'd propose to deprecate it in favour of _≄_?

[jamesmckinna]

Yes, I think so. It perhaps falls under a bikeshedding label, if we had one, but it seems like an avoidable wart in the 'fresh start' that (I think?) we want v2.0 to be... what's your view?

[JacquesCarette]

This seems quite sensible - using disparate symbols is confusing.

[jamesmckinna]

So there is a tension here (for me) between the 'formalistic' choice (take the formally negated symbol), and the 'semantic' choice (the negated equality is, in fact, a tight apartness relation, so that the rationals form a HeytingField, so a suitable choice would be _#_ for an apartness relation). For me, formal beats semantic, but in the interests of discussion...

[JacquesCarette]

Hmm, wouldn't proving that it is a tight apartness relation satisfy the semanticist in you? i.e. you first name the concept with the 'obvious' name, and then show that it has quite a bit more structure than naively expected. So then if you want to use it as an apartness relation, you can do it via using the HeytingField bundle, thus regaining the 'right' name?

[jamesmckinna]

(I think so, but all those various parts of me are at present exploding in all directions...)

[jamesmckinna]

And, regarding the deprecation, I think that the symbol should arise by suitably renaming the default negated-equality introduced by Setoid... but perhaps those dependencies don't quite cash out the way I might hope?