proposition: Lemma filterdirprod_imply : isfilter_imply filterdirprod.
proof: Proof. intros A B Himpl. apply hinhfun. 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. exists Ax, Ay. repeat split. + exact Fax. + exact Fay. + intros x y Hx Hy. now apply Himpl, Ha. Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA