Quotients are often used to describe new behavior. You could reasonably say that this ought to define a new type, but it's still an example of a meaningful coar

Quotients are often used to describe new behavior. You could reasonably say that this ought to define a new type, but it's still an example of a meaningful coarsening of equality. For example, to define rational numbers using only integers you take a rational to be a pair (n, d) but with a new equality such that (1, 2) and (2, 4) are equated.