[Agda] preserving predicate

[Serge D. Mechveliani]

On Sat, Feb 09, 2013 at 09:31:37PM +0400, Serge D. Mechveliani wrote:
> 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)
> ?
> [..]
 
Correction:      
  ... =  (p x) \equiv true -> (p y) \equiv true -> (p (x * y)) \equiv true

Or may be, to put    p : A -> Set l'


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