Definition PreFilterIntersection {X : UU} (FF : PreFilter X → hProp) : PreFilter X. Proof. intros. simple refine (make_PreFilter _ _ _ _). - apply (filterintersection _ FF). - apply filterintersection_imply. intros F _. apply filter_imply. - apply filterintersection_htrue. intros F _. apply filter_htrue. - apply filterintersection_and. intros F _. apply filter_and. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.