fact: Definition path_sigma_hprop_ap_pr1 {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.
imports: HoTT.Basics Types.Arrow Types.Paths