Prove [IsHSet hProp]

This is required to prove that the precategory of [hProp]s is strict.

We put the lemmas in `types/Universe.v` because we can't [Require Import
types.Universe.] in `HProp.v`, because `types/Universe.v` depeneds on
`HProp.v`.
Add an explicit lemma for [path_path_sigma]
Remove the [repeat match goal]

We only use each lemma one time, so we don't need it here.
Merge pull request #226 from JasonGross/trunc-hprop

Prove [IsHSet hProp]