Definition PreFilterTop {X : UU} : PreFilter X. Proof. simple refine (make_PreFilter _ _ _ _). - exact filtertop. - exact filtertop_imply. - exact filtertop_htrue. - exact filtertop_and. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.