HoTT/HoTT — pull request #361 by JasonGross (2014-04-07 00:35:09+00:00)
Title: 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.