Lemma filterdirprod_imply : isfilter_imply filterdirprod. 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.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.