Lemma filterbase_le {X : UU} (base base' : (X → hProp) → hProp) : (∏ P : X → hProp, base P → ∃ Q : X → hProp, base' Q × (∏ x, Q x → P x)) <-> (∏ P : X → hProp, filterbase base P → filterbase base' P). Proof. split. - intros Hbase P. apply hinhuniv. intros A. generalize (Hbase _ (pr1 (pr2 A))). apply hinhfun. intros B. exists (pr1 B). split. + apply (pr1 (pr2 B)). + intros x Bx. apply (pr2 (pr2 A)), (pr2 (pr2 B)), Bx. - intros Hbase P Hp. apply Hbase. apply hinhpr. now exists P. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.