[Agda] `Respects'

[Andrea Vezzosi]

Oh, that's much better

On Thu, Jan 22, 2015 at 2:26 PM, Arseniy Alekseyev
<arseniy.alekseyev at gmail.com> wrote:
> 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
>
>