Well, I think there's room for debate at the moment; equivalent objects can differ vis-a-vis judgmental equalities.  This whole revision got started because of a claimed judgmental equality in 6.10.12 which, it turns out, is not satisfied by any of our definitions of Z, though it is satisfied by the equivalent type N+1+N.  More generally, whenever we use the judgmental computation rule for an inductive type like List(A), we are using the fact that it's defined as a particular type rather than some equivalent one.  One might argue on this basis that judgmental equalities should be expunged from the theory, but that's not what we're doing in the first edition of the book.  So I think the most consistent thing to do here is to define "the set-quotient" as a particular HIT, and then say that the other definitions are equivalent (hence equal) to it.