HoTT/HoTT — pull request #354 by JasonGross (2014-03-31 00:57:25+00:00)
Title: 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.