Lemma FilterGenerated_correct {X : UU} : ∏ (L : (X → hProp) → hProp) (Hl : ∏ L' : Sequence (X → hProp), (∏ m, L (L' m)) → (∃ x : X, finite_intersection L' x)), (∏ A : X → hProp, L A → (FilterGenerated L Hl) A) × (∏ F : Filter X, (∏ A : X → hProp, L A → F A) → filter_le F (FilterGenerated L Hl)). Proof. intros L Hl. split. - intros A La. apply hinhpr. exists (singletonSequence A). split. + intros; assumption. + intros x Hx. apply (Hx (O,,paths_refl _)). - intros F Hf A. apply hinhuniv. intros Ha. refine (filter_imply _ _ _ _ _). + apply (pr2 (pr2 Ha)). + apply filter_finite_intersection. intros m. apply Hf. apply (pr1 (pr2 Ha)). Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.