fact: Definition equiv_path_sigma_hprop {A : Type} {P : A -> Type} {HP : forall a, IsHProp (P a)} (u v : sig P) : (u.1 = v.1) <~> (u = v) := Build_Equiv _ _ (path_sigma_hprop _ _) _.
imports: HoTT.Basics Types.Arrow Types.Paths