Lemma ex_filter_le {X : UU} : ∏ (F : Filter X) (A : X → hProp), (∑ G : Filter X, filter_le G F × G A) <-> (∏ B : X → hProp, F B → (∃ x : X, A x ∧ B x)). Proof. intros F A. split. - intros G B Fb. apply (filter_notempty (pr1 G)). apply filter_and. + apply (pr2 (pr2 G)). + now apply (pr1 (pr2 G)). - intros H. simple refine (tpair _ _ _). + simple refine (FilterGenerated _ _). * intros B. apply (F B ∨ B = A). * intros L Hl. assert (B : ∃ B : X → hProp, F B × (∏ x, (A x ∧ B x → A x ∧ finite_intersection L x))). { revert L Hl. apply (Sequence_rect (P := λ L : Sequence (X → hProp), (∏ m : stn (length L), (λ B : X → hProp, F B ∨ B = A) (L m)) → ∃ B : X → hProp, F B × (∏ x : X, A x ∧ B x → A x ∧ finite_intersection L x))). - intros Hl. apply hinhpr. rewrite finite_intersection_htrue. exists (λ _, htrue). split. + exact (filter_htrue F). + intros; assumption. - intros L B IHl Hl. rewrite finite_intersection_append. simple refine (hinhuniv _ _). 3: apply IHl. + intros C. generalize (Hl lastelement) ; simpl. rewrite append_vec_compute_2. apply hinhfun. apply sumofmaps ; [intros Fl | intros ->]. * refine (tpair _ _ _). split. ** apply (filter_and F). *** apply (pr1 (pr2 C)). *** apply Fl. ** intros x H0 ; repeat split. *** exact (pr1 H0). *** exact (pr2 (pr2 H0)). *** simple refine (pr2 (pr2 (pr2 C) x _)). split. **** exact (pr1 H0). **** exact (pr1 (pr2 H0)). * exists (pr1 C) ; split. ** exact (pr1 (pr2 C)). ** intros x H0 ; repeat split. *** exact (pr1 H0). *** exact (pr1 H0). *** simple refine (pr2 (pr2 (pr2 C) x _)). exact H0. + intros. generalize (Hl (dni_lastelement m)) ; simpl. rewrite <- replace_dni_last. now rewrite append_vec_compute_1. } revert B. apply hinhuniv. intros B. generalize (H (pr1 B) (pr1 (pr2 B))). apply hinhfun. intros x. exists (pr1 x). simple refine (pr2 (pr2 (pr2 B) (pr1 x) _)). exact (pr2 x). + split. * intros B Fb. apply hinhpr. exists (singletonSequence B). split. ** intros m. apply hinhpr. now left. ** intros x Hx. apply (Hx (O ,, paths_refl _)). * apply hinhpr. exists (singletonSequence A). split. ** intros m. apply hinhpr. now right. ** intros x Hx. apply (Hx (O ,, paths_refl _)). Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.