fact: Definition pr1_path_path_sigma_hprop {A : Type} {P : A -> Type} `{forall x, IsHProp (P x)} (u v : sig P) (p : u.1 = v.1) : (path_sigma_hprop u v p)..1 = p := eissect (path_sigma_hprop u v) p.
imports: HoTT.Basics Types.Arrow Types.Paths