Definition FilterBase {X : UU} (base : BaseOfFilter X) : Filter X. Proof. intros. exists (pr1 (PreFilterBase base)). split. - simple refine (pr2 (PreFilterBase base)). - apply filterbase_notempty. intros A Ha. simple refine (BaseOfFilter_notfalse _ _ _). + apply base. + apply Ha. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.