Lemma filterbase_and : isfilter_and filterbase. 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.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.