[Agda] Closed Predicate f in lib07

[Arseniy Alekseyev]

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