Two meanings of type constraint

The term "type constraint" tends to be overloaded for two very different concepts that should be distinguished:

  1. A constraint which is a boolean valued function allowing for a (restricted) set comprehension, and can be used to create new subtypes from existing types (aka specialisation by constraint). E.g. {x ∈ Z | x > 10}
  2. An equivalence relation over some set which defines a set of equivalence classes. E.g. this provides a basis for constructing the rationals out of Z⨯(Z\{0}) using the equivalence relation ~ satisfying (a,b)~(c,d) ⇔ ad=bc.

It doesn’t seem reasonable to think of 2) as a kind of 1). i.e. that equivalence classes be regarded as a subset of the original set. i.e. that equivalence classes be regarded as specialisation by constraint by using a boolean valued expression to obtain a canonical form. It's obscure to think of the rationals as a subtype of Z⨯(Z\{0}). Indeed if this were the case then why are possreps needed at all? All we need do is specialise tuple-types using set comprehension.