[Agda] `Respects'

[Sergei Meshveliani]

Thanks to people.
So, the library has not such a constructor.
And I am now going to introduce this:

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

 _Preserves1_ : ∀ {α p}{A : Set α} → (f : A → A) → (P : A → Set p) →
                                                            Set (α ⊔ p)
 f Preserves1 P = Preserves11 f P P


This will help in the case when  f or P  have a large expression.

------
Sergei



On Thu, 2015-01-22 at 13:26 +0000, Arseniy Alekseyev wrote:
> How about
> 
> 
> f Preserves1 P = f ∈ (P ⟨→⟩ P)
> 
> 
> ?
> 
> 
> 
> On 22 January 2015 at 13:21, Andrea Vezzosi <sanzhiyan at gmail.com>
> wrote:
>         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
>         _______________________________________________
>         Agda mailing list
>         Agda at lists.chalmers.se
>         https://lists.chalmers.se/mailman/listinfo/agda
>         
> 
>