Lemma PreFilterBase_le {X : UU} (base base' : BaseOfPreFilter X) : (∏ P : X → hProp, base P → ∃ Q : X → hProp, base' Q × (∏ x, Q x → P x)) <-> filter_le (PreFilterBase base') (PreFilterBase base). Proof. split. - intros Hbase P. apply (pr1 (filterbase_le base base')), Hbase. - apply (pr2 (filterbase_le base base')). Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.