Definition make_PreFilter {X : UU} (F : (X → hProp) → hProp) (Himpl : isfilter_imply F) (Htrue : isfilter_htrue F) (Hand : isfilter_and F) : PreFilter X := F,, Himpl,, isfilter_finite_intersection_carac F Htrue Hand.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.