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`.