proposition: Theorem total2_paths_hProp_equiv {A : UU} (B : A -> hProp) (x y : total2 (λ x, B x)) : (x = y) ≃ (pr1 x = pr1 y).
proof: Proof. intros. apply subtypeInjectivity. intro a. apply (pr2 (B a)). Defined.
imports: UniMath.Foundations.PartD