<div dir="ltr">How about<div><br></div><div><span style="font-size:12.8000001907349px">f Preserves1 P = </span>f ∈ (P ⟨→⟩ P)</div><div><br></div><div>?</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On 22 January 2015 at 13:21, Andrea Vezzosi <span dir="ltr"><<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Respects and Preserves are for binary predicates, there doesn't seem<br>
to be a version for unary ones.<br>
<br>
You can write something like this if you like, which of course is<br>
ultimately the same as writing it directly:<br>
<br>
open import Relation.Unary<br>
<br>
_▸_ : ∀ {A : Set} → (A → Set) → (A → A) → A → Set<br>
P ▸ f = \ a → P (f a)<br>
<br>
_Preserves1_ : ∀ {A} (f : A → A) P → Set<br>
f Preserves1 P = Universal (P ⇒ (P ▸ f))<br>
<br>
Cheers,<br>
Andrea<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
On Wed, Jan 21, 2015 at 8:55 PM, Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>> wrote:<br>
> Who knows, please,<br>
><br>
> what has Standard library to express the type constructor<br>
><br>
> \ (P : A → Set) (f : A → A) → (∀ {x} → P x → P (f x))<br>
> ?<br>
><br>
> (f Respects P), (f Preserves P) do not seem to fit.<br>
><br>
> Thanks,<br>
><br>
> ------<br>
> Sergei<br>
><br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>