[Agda] `Respects'

[Arseniy Alekseyev]

How about

f Preserves1 P = f ∈ (P ⟨→⟩ P)

?


On 22 January 2015 at 13:21, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:

> Respects and Preserves are for binary predicates, there doesn't seem
> to be a version for unary ones.
>
> You can write something like this if you like, which of course is
> ultimately the same as writing it directly:
>
> open import Relation.Unary
>
> _▸_ : ∀ {A : Set} → (A → Set) → (A → A) → A → Set
> P ▸ f = \ a → P (f a)
>
> _Preserves1_ : ∀ {A} (f : A → A) P → Set
> f Preserves1 P = Universal (P ⇒ (P ▸ f))
>
> Cheers,
> Andrea
>
>
> On Wed, Jan 21, 2015 at 8:55 PM, Sergei Meshveliani <mechvel at botik.ru>
> wrote:
> > Who knows, please,
> >
> > what has Standard library to express the type constructor
> >
> >   \ (P : A → Set) (f : A → A) → (∀ {x} → P x → P (f x))
> > ?
> >
> > (f Respects P), (f Preserves P)   do not seem to fit.
> >
> > Thanks,
> >
> > ------
> > Sergei
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150122/1f4cbcfe/attachment.html