Definition FilterTop {X : UU} (x0 : ∥ X ∥) : Filter X. Proof. refine (tpair _ _ _). split. - apply (pr2 PreFilterTop). - apply filtertop_notempty, x0. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.