Lemma base_finite_intersection : ∏ L : Sequence (X → hProp), (∏ n, base (L n)) → ∃ A, base A × (∏ x, A x → finite_intersection L x). Proof. intros L Hbase. apply (pr2 (finite_intersection_hProp (λ B, ∃ A : X → hProp, base A × (∏ x : X, A x → B x)))). - split. + revert Hempty. apply hinhfun. intros A. now exists (pr1 A), (pr2 A). + intros A B. apply hinhuniv2. intros A' B'. generalize (Hand _ _ (pr1 (pr2 A')) (pr1 (pr2 B'))). apply hinhfun. intros C. exists (pr1 C). split. * exact (pr1 (pr2 C)). * intros x Cx. split. ** apply (pr2 (pr2 A')), (pr1 (pr2 (pr2 C) _ Cx)). ** apply (pr2 (pr2 B')), (pr2 (pr2 (pr2 C) _ Cx)). - intros n. apply hinhpr. exists (L n). split. + now apply Hbase. + intros; assumption. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.