Lemma filterdirprod_and : isfilter_and filterdirprod. Proof. intros A B. apply hinhfun2. intros C D. 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 (pr1 D) (pr1 (pr2 D)) (pr1 (pr2 (pr2 D))) (pr1 (pr2 (pr2 (pr2 D)))) (pr2 (pr2 (pr2 (pr2 D)))) ; clear D ; intros Bx By Fbx Fby Hb. exists (λ x : X, Ax x ∧ Bx x), (λ y : Y, Ay y ∧ By y). repeat split. + now apply Hand_x. + now apply Hand_y. + apply Ha. * apply (pr1 X0). * apply (pr1 X1). + apply Hb. * apply (pr2 X0). * apply (pr2 X1). Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.