Definition FilterIntersection {X : UU} (FF : Filter X → hProp) (Hff : ∃ F : Filter X, FF F) : Filter X. Proof. simple refine (make_Filter _ _ _ _ _). - apply (filterintersection _ FF). - apply filterintersection_imply. intros F _. apply (filter_imply (pr1Filter _ F)). - apply filterintersection_htrue. intros F _. apply (filter_htrue (pr1Filter _ F)). - apply filterintersection_and. intros F _. apply (filter_and (pr1Filter _ F)). - apply filterintersection_notempty. + intros F _. apply (filter_notempty F). + exact Hff. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.