{A : Type} {P : A -> Type} `{forall x, IsHProp (P x)} (u v : sig P) (p : u = v) : path_sigma_hprop u v (ap pr1 p) = p := eisretr (path_sigma_hprop u v) p.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.