Definition PreFilterBase {X : UU} (base : BaseOfPreFilter X) : PreFilter X. Proof. simple refine (make_PreFilter _ _ _ _). - apply (filterbase base). - apply filterbase_imply. - apply filterbase_htrue, BaseOfPreFilter_notempty. - apply filterbase_and. intros A B. now apply BaseOfPreFilter_and. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.