[Agda] Closed Predicate f in lib07

[Arseniy Alekseyev]

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

Regards,
Arseniy