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

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