proposition: Lemma filterbase_imply : isfilter_imply filterbase.
proof: Proof. intros A B H. apply hinhfun. intros A'. exists (pr1 A'). split. - apply (pr1 (pr2 A')). - intros x Hx. apply H. now apply (pr2 (pr2 A')). Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA