[Agda] Closed Predicate f in lib07

Sergei Meshveliani mechvel at botik.ru
Sat Aug 31 13:50:36 CEST 2013

```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

```