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.

Apologies if this is already somewhere in the library; I could not find it.