Definition pr1BaseOfFilter {X : UU} : BaseOfFilter X → BaseOfPreFilter X. Proof. intros base. exists (pr1 base). split. - apply (pr1 (pr2 base)). - apply (pr1 (pr2 (pr2 base))). Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.