Definition filterdom : (X → hProp) → hProp := λ A : X → hProp, F (λ x : X, make_hProp (dom x → A x) (isapropimpl _ _ (propproperty _))).
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.