Definition pr1Filter (X : UU) (F : Filter X) : PreFilter X := pr1 F,, pr1 (pr2 F).
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.