[Agda] `Respects'

[Andrés Sicard-Ramírez]

On 21 January 2015 at 14:55, Sergei Meshveliani <mechvel at botik.ru> wrote:

> what has Standard library to express the type constructor
>
>   \ (P : A → Set) (f : A → A) → (∀ {x} → P x → P (f x))
> ?
>

​This is not ​valid, e.g.

A = ℕ
P n = Even n
​f​ n = n + 1


-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150122/3ceb10f1/attachment.html