Prove that [ap pr1] is an equivalence for [HProp] and [HSet]

It's possible this could be factored through [issig_hProp] and an
analogous [issig_hSet].  But I'm lazy.

This is useful for proving that the precategory of sets is a category.