Definition PreFilterDirprod {X Y : UU} (Fx : PreFilter X) (Fy : PreFilter Y) : PreFilter (X × Y). Proof. simple refine (make_PreFilter _ _ _ _). - exact (filterdirprod Fx Fy). - apply filterdirprod_imply. - apply filterdirprod_htrue. + apply filter_htrue. + apply filter_htrue. - apply filterdirprod_and. + apply filter_and. + apply filter_and. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.