proposition: Lemma filterdirprod_notempty : isfilter_notempty filterdirprod.
proof: Proof. intros A. apply hinhuniv. intros C. generalize (pr1 C) (pr1 (pr2 C)) (pr1 (pr2 (pr2 C))) (pr1 (pr2 (pr2 (pr2 C)))) (pr2 (pr2 (pr2 (pr2 C)))) ; clear C ; intros Ax Ay Fax Fay Ha. generalize (Hempty_x _ Fax) (Hempty_y _ Fay). apply hinhfun2. intros x y. exists (pr1 x,,pr1 y). apply Ha. - exact (pr2 x). - exact (pr2 y). Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA