search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
583 stars 236 forks source link

Inconsistent naming between `Data.(Nat/Integer).Properties` #1579

Open MatthewDaggitt opened 3 years ago

MatthewDaggitt commented 3 years ago

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 commented 3 years ago

Also Antimonotonic etc.

jamesmckinna commented 1 year ago

See also #2087 / #2089

jamesmckinna commented 1 year ago

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.