Definition FilterGenerated {X : UU} (L : (X → hProp) → hProp) (Hl : ∏ L' : Sequence (X → hProp), (∏ m : stn (length L'), L (L' m)) → ∃ x : X, finite_intersection L' x) : Filter X. Proof. exists (PreFilterGenerated L). split. - apply (pr2 (PreFilterGenerated L)). - apply filtergenerated_notempty. exact Hl. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.