Lemma filterbase_genetated : filterbase = filtergenerated base. Proof. apply funextfun ; intros P. apply hPropUnivalence. - apply hinhfun. intros A. exists (singletonSequence (pr1 A)). split. + intros m ; simpl. exact (pr1 (pr2 A)). + intros x Ax. apply (pr2 (pr2 A)). simple refine (Ax _). now exists 0%nat. - apply hinhuniv. intros L. generalize (base_finite_intersection (pr1 L) (pr1 (pr2 L))). apply hinhfun. intros A. exists (pr1 A) ; split. + exact (pr1 (pr2 A)). + intros x Ax. now apply (pr2 (pr2 L)), (pr2 (pr2 A)). Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.