[Agda] preserving predicate

[Serge D. Mechveliani]

People,
does there exist a library item which is close to 

  Closed_2 : \forall {l} {A : Set l} (A -> Bool) -> Op_2 A -> Set _
  Closed_2 p _*_ =  p x -> p y -> p (x * y)
?

(for example, this expresses that a subset in A is closed by _*_).

Thanks,

------
Sergei