Definition PreFilter (X : UU) := ∑ (F : (X → hProp) → hProp), isPreFilter F.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.