Definition FilterDirprod {X Y : UU} (Fx : Filter X) (Fy : Filter Y) : Filter (X × Y). Proof. refine (tpair _ _ _). split. - apply (pr2 (PreFilterDirprod Fx Fy)). - apply filterdirprod_notempty. + apply filter_notempty. + apply filter_notempty. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.