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