Define a variant of [path_sigma] for hprops

In this case, we don't need to provide the second projection.

Also prove that it's an equivalence.

Also move [equiv_path_sigma_hprop] to HProp.v, because it fits there,
and fits in nicely with the proof.