Definition isfilter_and := ∏ A B : X → hProp, F A → F B → F (λ x : X, A x ∧ B x).
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.