[Agda] preserving predicate

[Nils Anders Danielsson]

On 2013-02-09 18:38, Serge D. Mechveliani wrote:
> 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'

You could perhaps use Relation.Binary._Preserves₂_⟶_⟶_, but I suspect
that the code is clearer if you just write down what you mean directly:

   _Preserves₂_⟶_⟶_ :
     ∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c} →
     (A → B → C) → Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → Set _
   _+_ Preserves₂ P ⟶ Q ⟶ R =
     ∀ {x y u v} → P x y → Q u v → R (x + u) (y + v)

-- 
/NAD