Definition filterim := λ A : (Y → hProp), F (λ x : X, A (f x)).
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.