Lemma finite_intersection_htrue {X : UU} : finite_intersection nil = (λ _ : X, htrue). Proof. apply funextfun ; intros x. apply hPropUnivalence. - intros _. apply tt. - intros _ m. generalize (pr1 m) (pr2 m). intros m' Hm. apply fromempty. revert Hm. apply negnatlthn0. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Subtypes.