[Agda] Closed Predicate f in lib07
Arseniy Alekseyev
arseniy.alekseyev at gmail.com
Sat Aug 31 18:18:41 CEST 2013
Sorry Sergei,
I failed to note the difference between binary and unary predicates in
the types.
Now I think you may want to look at the module Relation.Unary where you
can find this:
_⟨→⟩_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
Pred A ℓ₁ → Pred B ℓ₂ → Pred (A → B) _
(P ⟨→⟩ Q) f = P ⊆ Q ∘ f
It allows you to define:
Closed : ∀ {a p} {A : Set a} → (A → Set p) → (A → A) → Set _
Closed P = P ⟨→⟩ P
Closed₂ : ∀ {a p} {A : Set a} → (A → Set p) → (A → A → A) → Set _
Closed₂ P = P ⟨→⟩ P ⟨→⟩ P
This time I did use the compiler to verify my claims!
Cheers!
Arseniy
More information about the Agda
mailing list