Lemma PreFilterGenerated_correct {X : UU} : ∏ (L : (X → hProp) → hProp), (∏ A : X → hProp, L A → (PreFilterGenerated L) A) × (∏ F : PreFilter X, (∏ A : X → hProp, L A → F A) → filter_le F (PreFilterGenerated L)). Proof. intros L. 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.