Definition filterdirprod : (X × Y → hProp) → hProp := λ A : (X × Y) → hProp, ∃ (Ax : X → hProp) (Ay : Y → hProp), Fx Ax × Fy Ay × (∏ (x : X) (y : Y), Ax x → Ay y → A (x,,y)).
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.