HoTT/HoTT — pull request #552 by mikeshulman (2014-10-03 20:38:49+00:00)
Title: quotient_rect requires its motive to be an hset; close #551

The main neccesary consequence is that `in_class` has to be defined by quotient-recursion into `A -> hProp` rather than `A -> Type`, since the former is a set while the latter isn't, and moreover this requires univalence. The change to the definition of `quotient_surjective` is to free it from a consequent dependence on univalence; possibly analogous changes could be made to some other functions, but I was going for the minimal changes needed to fix this bug.