[Agda] `Respects'

[Andrea Vezzosi]

Respects and Preserves are for binary predicates, there doesn't seem
to be a version for unary ones.

You can write something like this if you like, which of course is
ultimately the same as writing it directly:

open import Relation.Unary

_▸_ : ∀ {A : Set} → (A → Set) → (A → A) → A → Set
P ▸ f = \ a → P (f a)

_Preserves1_ : ∀ {A} (f : A → A) P → Set
f Preserves1 P = Universal (P ⇒ (P ▸ f))

Cheers,
Andrea


On Wed, Jan 21, 2015 at 8:55 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> Who knows, please,
>
> what has Standard library to express the type constructor
>
>   \ (P : A → Set) (f : A → A) → (∀ {x} → P x → P (f x))
> ?
>
> (f Respects P), (f Preserves P)   do not seem to fit.
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda