Definition PreFilterDom {X : UU} (F : PreFilter X) (dom : X → hProp) : PreFilter X. Proof. simple refine (make_PreFilter _ _ _ _). - exact (filterdom F dom). - apply filterdom_imply, filter_imply. - apply filterdom_htrue. + apply filter_imply. + apply filter_htrue. - apply filterdom_and. + apply filter_imply. + apply filter_and. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.