[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
More information about the Agda
mailing list