[Agda] Closed Predicate f in lib07

[Sergei Meshveliani]

On Sat, 2013-08-31 at 14:37 +0400, Sergei Meshveliani wrote:
> On Sat, 2013-08-31 at 04:34 +0100, Arseniy Alekseyev wrote:
> > Dear Sergei,
> > 
> > The standard library does have similar functions in
> > module Relation.Binary.Core:
> > 
> >   _Preserves_⟶_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
> >                   (A → B) → Rel A ℓ₁ → Rel B ℓ₂ → Set _
> > 
> >   _Preserves₂_⟶_⟶_ :
> >     ∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c} →
> >     (A → B → C) → Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → Set _
> > 
> > You can use those to express Closed and Closed2:
> > 
> >   Closed P f = f Preserves P ⟶ P
> >   Closed₂ P _*_ = _*_ Preserves₂ P ⟶ P ⟶ P
> > [..]
> 
> 
> I knew about these functions, but I did not recall about easy conversion
> from  unary P to a binary relation. Because I have  P : A -> Set p.
> 
> So, lib-0.7 does help here. For example, the first definition becomes
>  
>  Closed : ∀ {a p} {A : Set a} → (A → Set p) → (A → A) → Set (p ⊔L a)
>                                            
>  Closed P f =  f Preserves _~_ ⟶ _~_   where _~_ = \ x _ → P x
> [..]


Still, this occurs not so simple.
With this definition, the usage of  Closed₂  is like this:

  ...
  postulate closed : Closed₂ {_} {_} {baseCarrier} member _∙_
                                                                               
  _∙s_ : Op₂ subcarrier
  (subsetEl x mem-x) ∙s (subsetEl y mem-y) =  subsetEl xy member-xy
                     where
	             xy = x ∙ y
                     member-xy = closed {x} {x} {y} {y} mem-x mem-y

The checker forces me to insert this    ``{x} {x} {y} {y}'',

probably because  Preserves₂  has the three domains:  A, B, C.
I do not know how to write it shorter.
And the definition 

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

allows to write there       ``closed mem-x mem-y''.
So, I tend to directly use 
                            ∀ {x y} → P x → P y → P (x * y)

(for this case) rather than  Preserves₂.

Regards,

------
Sergei