proposition: Lemma filterbase_and : isfilter_and filterbase.
proof: Proof. intros A B. apply hinhuniv2. intros A' B'. refine (hinhfun _ _). 2: apply Hand. 2: (apply (pr1 (pr2 A'))). 2: (apply (pr1 (pr2 B'))). intros C'. exists (pr1 C'). split. - apply (pr1 (pr2 C')). - intros x Cx ; split. + apply (pr2 (pr2 A')). now refine (pr1 (pr2 (pr2 C') _ _)). + apply (pr2 (pr2 B')). now refine (pr2 (pr2 (pr2 C') _ _)). Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA