Definition filtersubtype : ((∑ x : X, dom x) → hProp) → hProp := λ A : (∑ x : X, dom x) → hProp, F (λ x : X, make_hProp (∏ Hx : dom x, A (x,, Hx)) (impred_isaprop _ (λ _, propproperty _))).
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.