Definition FilterSubtype {X : UU} (F : Filter X) (dom : X → hProp) (Hdom : ∏ P, F P → ∃ x, dom x ∧ P x) : Filter (∑ x : X, dom x). Proof. refine (tpair _ _ _). split. - apply (pr2 (PreFilterSubtype F dom)). - apply filtersubtype_notempty. exact Hdom. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.