Definition BaseOfFilter (X : UU) := ∑ (base : (X → hProp) → hProp), isBaseOfFilter base.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.