# [Agda] preserving predicate

Serge D. Mechveliani mechvel at botik.ru
Sat Feb 9 18:38:31 CET 2013

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