[Agda] Closed Predicate f in lib07
Sergei Meshveliani
mechvel at botik.ru
Sat Aug 31 12:37:00 CEST 2013
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
More information about the Agda
mailing list