proposition: Lemma emptynofilter : ∏ F : (empty → hProp) → hProp, ¬ isFilter F.
proof: 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.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA