Lemma eq_equalities_between_pairs (A : UU) (B : A -> UU)(x y : total2 (λ x, B x)) (p q : x = y) (H : base_paths _ _ p = base_paths _ _ q) (H2 : transportf (fun p : pr1 x = pr1 y => transportf _ p (pr2 x) = pr2 y ) H (fiber_paths p) = fiber_paths q) : p = q. Proof. apply (invmaponpathsweq (total2_paths_equiv _ _ _ )). apply (total2_paths_f (B:=(fun p : pr1 x = pr1 y => transportf (λ x : A, B x) p (pr2 x) = pr2 y)) (s := (total2_paths_equiv B x y) p) (s' := (total2_paths_equiv B x y) q) H). assumption. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.