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'...

[jamesmckinna]

Aaaargh! The various definitions do exist in Relation.Binary.Definitions, but aren't then specialised in Algebra.Definitions (and perhaps that wouldn't make sense as such to do so...?).

Monotonic₁ : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → Set _
Monotonic₁ _≤_ _⊑_ f = f Preserves _≤_ ⟶ _⊑_

Antitonic₁ : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → Set _
Antitonic₁ _≤_ _⊑_ f = f Preserves (flip _≤_) ⟶ _⊑_

Monotonic₂ : Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → (A → B → C) → Set _
Monotonic₂ _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ _≤_ ⟶ _⊑_ ⟶ _≼_

MonotonicAntitonic : Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → (A → B → C) → Set _
MonotonicAntitonic _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ _≤_ ⟶ (flip _⊑_) ⟶ _≼_

AntitonicMonotonic : Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → (A → B → C) → Set _
AntitonicMonotonic _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ (flip _≤_) ⟶ _⊑_ ⟶ _≼_

Antitonic₂ : Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → (A → B → C) → Set _
Antitonic₂ _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ (flip _≤_) ⟶ (flip _⊑_) ⟶ _≼_

Looking at these, I can't help wondering if we should rephrase everything in terms of Monotonic₁ and Monotonic₂ together with judicious use of flip... any reason why things are (often?) inlined like this in the library, and thus avoid direct appeal to (higher-level) 'symmetries'?

[JacquesCarette]

My guess why it's this way: history. Things were developed "by hand" and only slowly did patterns emerge. You could say that those patterns should be well-known - and indeed they are to the people whose educational path included enough of the right kind of Algebra. But that doesn't tend to be the same people as those who develop ITPs! [I've seen the same thing happen in CASes, but there it's mostly about not knowing enough analysis.]

[MatthewDaggitt]

#2580 shouldn't close this issue right?

[jamesmckinna]

#2580 shouldn't close this issue right?

No, you're correct, but it might do once that DRAFT PR is finished?
In any case, will tweak the preamble to it to remove the fixes cue for the time being... hmmm doesn't seem to have worked?

[jamesmckinna]

Progress so far on #2580 suggests that at least the various Data.X.Properties module are mutually consistent, in naming lemmas vs. the 'opposite' handedness in the lemma statements... so we should only consider a breaking change after resolving the discussion on #2532 ?