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