Definition weqpr1_irr_sec {X} {P:X->Type} (irr:∏ x (p q:P x), p = q) (sec:∏ x, P x) : weq (total2 P) X. Proof. intros. set (isc := λ x, iscontraprop1 (invproofirrelevance _ (irr x)) (sec x)). apply Equivalence_to_weq. simple refine (makeEquivalence _ _ _ _ _ _ _). { exact pr1. } { intro x. exact (x,,sec x). } { intro x. reflexivity. } { intros [x p]. simpl. apply maponpaths. apply irr. } { intros [x p]. simpl. apply pair_path_in2_comp1. } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Equivalences.