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