Definition PreFilterGenerated {X : UU} (L : (X → hProp) → hProp) : PreFilter X. Proof. simple refine (make_PreFilter _ _ _ _). - apply (filtergenerated L). - apply filtergenerated_imply. - apply filtergenerated_htrue. - apply filtergenerated_and. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.