proposition: Lemma filter_const : ∏ A : hProp, F (λ _ : X, A) → ¬ (¬ A).
proof: Proof. intros A Fa Ha. generalize (filter_notempty _ Fa). apply factor_through_squash. - apply isapropempty. - intros x ; generalize (pr2 x); clear x. exact Ha. Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA