{A : Type} {P : A -> Type} `{forall x, IsHProp (P x)} (u : sig P) : path_sigma_hprop u u 1 = 1. Proof. unfold path_sigma_hprop. unfold isequiv_pr1_contr; simpl. refine (ap (fun p => match p in (_ = v2) return (u = (u.1; v2)) with 1 => 1 end) (contr (idpath u.2))). Defined.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.