[Agda] Closed Predicate f in lib07

[Sergei Meshveliani]

People,
I define

  Closed : ∀ {a p} {A : Set a} → (A → Set p) → (A → A) → Set _
  Closed P f =  ∀ {x} → P x → P (f x)

to express that a predicate P is closed under  f : A -> A,


  Closed₂ : ∀ {a p} {A : Set a} → (A → Set p) → Op₂ A → Set _
  Closed₂ P _*_ =  ∀ {x y} → P x → P y → P (x * y)

to express that a predicate P is closed under  _*_ : Op₂ A.
For example, a subsemigroup carrier membership is closed under the
semigroup operation _*_.

Now, the Standard library  lib-0.7  has 
                           _Respects_, _Respects₂_, _Preserves_ ...

Has it something to express  Closed, Closed₂ ?

Thanks,

------
Sergei