Lemma finite_intersection_1 {X : UU} : ∏ (A : X → hProp), finite_intersection (singletonSequence A) = A. Proof. intros A. apply funextfun ; intros x. apply hPropUnivalence. - intros H. simple refine (H _). now exists 0. - intros Lx m. exact Lx. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Subtypes.