Lemma filter_const : ∏ A : hProp, F (λ _ : X, A) → ¬ (¬ A). 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.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.