[Agda] `Respects'

Sergei Meshveliani mechvel at botik.ru
Wed Jan 21 20:55:05 CET 2015


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



More information about the Agda mailing list