A name for ``P x → P (f x)``

[mechvel]

For P : Pred A _, f : A → A,
what is the standard library type definition for {x : A} → P x → P (f x)
?
A natural definition would be f Preserves P, but _Preserves_ is for _≈_. Congruent also is for equality.
May be, introduce _PreservesPred_ ?
Like this:

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

_PreservesPred_ : ∀ {α p}{A : Set α} → (A → A) → Pred A p → Set (α ⊔ p)
f PreservesPred P =  PreservesPreds f P P

[gallais]

Note that you can quickly write something equivalent using the Relation.Unary
combinators: ∀[ P ⇒ f ⊢ P ].

[laMudri]

Do you think it's worth adding a README file for the Relation.Unary combinators? Perhaps not, but I'm not sure how to learn them without reading one of your papers. In particular, I don't think I'd really know to look for _⊢_ (as @mechvel presumably didn't).

[mechvel]

I would like more _PreservesPred_.

[jamesmckinna]

Two {comment/question}s:

• agree re Relation.Unary: eg why Satisfiable rather than Inhabited? (which might be more to the taste of constructivists?)
• rather than _PreservesPred_, might consider better _-Consistent_, and its converse _-Closed_ so that one is (more) naturally put in mind of the infinitary (Knaster-Tarski) lattice-theoretic aspects of Pred_, which are less well developed in Relation.Unary.Properties, it seems
  Would the latter (lattice-theoretic aspects of Pred, _ ⊆_) perhaps make for a more fruitful Issue to open than this one?

[gallais]

@jamesmckinna We do have some of these things, following from our discussions :)
http://agda.github.io/agda-stdlib/Relation.Unary.Closure.Base.html
http://agda.github.io/agda-stdlib/Relation.Unary.Closure.Preorder.html
http://agda.github.io/agda-stdlib/Relation.Unary.Closure.StrictPartialOrder.html

[jamesmckinna]

@gallais 🤦
I'm already regretting the comment, because the two senses of Closed, namely that the Pred is closed under taking f-images, and the Knaster-Tarski definition, that the Pred is a [Pre-|Post-]Fixedpoint (authors differ, so I avoided that discussion...) under f*, seem in conflict... or else it's too late and I should leave the office and go home.

[mechvel]

In mathematics, they say just during centuries "a map f preserves the relation R"
(at least in Russian translation).

[jamesmckinna]

@mechvel Indeed... I suppose my only point, for what it is worth, is that each of these concepts can/will/might have many different names, depending on the particular 'deployment' context of the user concerned. @laMudri and @gallais 's suggestions indicate that lower-level primitives are available on top of which any/each of us might make suitable definitions for our own purposes. Library designers (I am not one, merely a contributor, but one who has seen discussions of this kind go round and round in circles for 30+ years) might want us to try to keep the library as rich as possible, while not over-committing an already crowded namespace with choices which conflict with other, elsewhere established, usages. The richness of mathematics and mathematical language in part arises (happily!) from the natural human capacity to overload terminology, and rely on huge amounts of (local) contextual information in order to be able to disambiguate... while a library design(er) needs to balance (less happily, perhaps) a more complicated set of global constraints/trade-offs.