fact: Definition BaseOfFilter (X : UU) := ∑ (base : (X → hProp) → hProp), isBaseOfFilter base.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA