Lemma filterdirprod_htrue : isfilter_htrue filterdirprod. Proof. apply hinhpr. exists (λ _:X, htrue), (λ _:Y, htrue). repeat split. + apply Htrue_x. + apply Htrue_y. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.