Lemma finite_intersection_and {X : UU} : ∏ A B : X → hProp, finite_intersection (pairSequence A B) = (λ x : X, A x ∧ B x). Proof. intros A B. apply funextfun ; intro x. apply hPropUnivalence. - intros H. split. + simple refine (H (0,,_)). reflexivity. + simple refine (H (1,,_)). reflexivity. - intros H m ; simpl. change m with (pr1 m,,pr2 m). generalize (pr1 m) (pr2 m). clear m. intros m Hm. induction m as [ | m _]. + apply (pr1 H). + apply (pr2 H). Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Subtypes.