Definition isPreFilter {X : UU} (F : (X → hProp) → hProp) := isfilter_imply F × isfilter_finite_intersection F.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.