[Agda] Closed Predicate f in lib07

[Sergei Meshveliani]

On Sat, 2013-08-31 at 04:34 +0100, Arseniy Alekseyev wrote:
> Dear Sergei,
> 
> The standard library does have similar functions in
> module Relation.Binary.Core:
> 
>   _Preserves_⟶_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
>                   (A → B) → Rel A ℓ₁ → Rel B ℓ₂ → Set _
> 
>   _Preserves₂_⟶_⟶_ :
>     ∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c} →
>     (A → B → C) → Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → Set _
> 
> You can use those to express Closed and Closed2:
> 
>   Closed P f = f Preserves P ⟶ P
>   Closed₂ P _*_ = _*_ Preserves₂ P ⟶ P ⟶ P
> [..]


I knew about these functions, but I did not recall about easy conversion
from  unary P to a binary relation. Because I have  P : A -> Set p.

So, lib-0.7 does help here. For example, the first definition becomes
 
 Closed : ∀ {a p} {A : Set a} → (A → Set p) → (A → A) → Set (p ⊔L a)
                                           
 Closed P f =  f Preserves _~_ ⟶ _~_   where _~_ = \ x _ → P x

Thank you,

------
Sergei