Definition PreFilterSubtype {X : UU} (F : PreFilter X) (dom : X → hProp) : PreFilter (∑ x : X, dom x). Proof. simple refine (make_PreFilter _ _ _ _). - exact (filtersubtype F dom). - apply filtersubtype_imply, filter_imply. - apply filtersubtype_htrue. + apply filter_imply. + apply filter_htrue. - apply filtersubtype_and. + apply filter_imply. + apply filter_and. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.