Lemma emptynofilter : ∏ F : (empty → hProp) → hProp, ¬ isFilter F. Proof. intros F Hf. generalize (isfilter_finite_intersection_htrue _ (pr2 (pr1 Hf))) ; intros Htrue. generalize (pr2 Hf _ Htrue). apply factor_through_squash. - apply isapropempty. - intros x. apply (pr1 x). Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.