Inconsistent naming between Data.(Nat/Integer).Properties

[MatthewDaggitt]

We have our left and rights switched round in *-monoʳ-≤, *-monoʳ-≤-pos. It would be kind of good if we had definitions for Monotonic/LeftMonotonic/RightMonotonic etc. in Relation.Binary.Definitions to help keep us on the straight and narrow.

[MatthewDaggitt]

Also Antimonotonic etc.

[jamesmckinna]

See also #2087 / #2089

[jamesmckinna]

Regarding Anti, I have the (slight? vague?) feeling that as with Cancellative, it might be better to parametrise these properties on 'source' and 'target' relations... cf. Preserves?

UPDATED: I had been looking at this from the vantage point of Algebra.Definitions rather than Relation.Binary.Definitions... and am now struck by the witting/unwitting duplication between the two. As an example, the definition in the latter of AntiSym might as well be (towards a) definition of generalised monotonicity but for the distinction between type/level polymorphism in the Relation hierarchy, vs. the singly-sorted/typed approach (for a fixed 'equality' relation!) of Algebra...

I have unpushed commits on https://github.com/jamesmckinna/agda-stdlib/tree/NumericNonZeroEquivalents
towards a See PR #2117 for a branch addressing this issue and related matters #1175 #1436 #1562, but currently trying to figure out the 'best' import strategy for all these (overlapping!) concepts... but I'm a bit basically completely burnt out tbh right now.

[jamesmckinna]

Also Antimonotonic etc.

Are we sure we need this? Monotonicity is/should be usually stated wrt two distinct orderings, and these can then be varied as:

• same, same: 'usual' monotonicity within a given ordered structure
• same, flipped: antitone
• etc.

[jamesmckinna]

See also #2532 for the wider issue of the (need to agree the) semantics of 'left' and 'right'...