Suggestion with `Preserves` for two predicates

[mechvel]

lib-2.3 has Preserves for the pair of a binary relation and a map.
But such is also needed for one or two predicates.
For example, I define

Preserves11 :     ∀ {β p q}{B : Set β} → (A → B) → Pred A p → Pred B q → Set _                  
Preserves11 f P Q =  ∀ {x} → P x → Q (f x)                                      
                                                                                
_Preserves_ :  ∀ {p} → (A → A) → Pred A p → Set (α ⊔ p)                         
f Preserves P =  ∀ {x} → P x → P (f x)                                          

For example, Preserves11 Integer.+_ Even-ℕ Even-ℤ

means (if {n : ℕ} is even, then (+ n) : ℤ is even in ℤ).

And this cannot be named Respects* or Congruent* due to the library style.
May this have sense for Standard library?

[jamesmckinna]

I could imagine this being a useful addition to Relation.Unary, so if you raise a PR, we would look at it.

That said, please also look at the existing definitions #2840 and properties #2866 of unary adjoints... where your Preserves11 property is/would be expressible in terms of existing Relation.Unary constructions as P ⊆ f ⊢ Q, so I'd be just as likely to say that the library doesn't need (Fairbairn threshold) to add this as a named definition.

Similarly, one could argue that a more general definition would be better, namely in terms of Relation.Binary._⟶_Respects_, as Preserves11 f P Q = P ⟶ Q Respects λ x y → y ≡ f x, using the graph binary relation associated with f, which at least generalises to the case of non-Propositional equality λ x y → y ≈ f x.

I definitely agree that the library is 'biased' towards definitions and properties of Binary relations more than Unary predicates, so an initiative to refactor both to make them more uniform/comparable might well yield an improved overall design...

[mechvel]

On 2026-01-22 13:22, jamesmckinna wrote: jamesmckinna left a comment (agda/agda-stdlib#2909) [1] I could imagine this being a useful addition to Relation.Unary, so if you raise a PR, we would look at it. [..]

So far, I am going to use Preserves11 of my own. But if you find that this my suggestion is reasonable and thus make the corresponding change in the next lib version, then I have to see this in CHANGELOG, and may be change my code to something more close to Standard. Regards, SM