Equivalence classes

equivalence class It is noteworthy that quotient types offer a computationally tractable way of treating topics normally expressed in terms of equivalence classes. For example, if we want to study the algebraic properties of ${{\mathbb{Z} }} /\!/ mod\ n$it is customary to form the set of equivalence classes of ${{\mathbb{Z} }}$ where the equivalence class of an element z is $[z]=\left\{i\!:\!{{\mathbb{Z} }}\ \vert\ i=z\ mod\ n\right\}$. The set of these classes is denoted ${{\mathbb{Z} }} / mod\ n$. The algebraic operations are extended to classes by

[z₁] + [z₂] = [z₁ + z₂],

$[z_1] \star [z_2] = [z_1 \star z_2]$,    etc.

All of this development can be rephrased in terms quotient types. We show that + and $\star$ are well-defined on ${{\mathbb{Z} }} /\!/ mod\ n$, and the elements are ordinary integers instead of equivalence classes. What changes is the equality on elements.