fact: Definition isFilter {X : UU} (F : (X → hProp) → hProp) := isPreFilter F × isfilter_notempty F.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA