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.
Probably we could, but in general the unbundled approach seems better.