A quotient type defines an equivalence relation
In type theories which allow quotient types, an additional requirement is made that all operations must respect the equivalence between elements.
In the early 1980s, quotient types were defined and implemented as part of the Nuprl proof assistant, in work led by Robert L. Constable and others.
[3] Quotient types can be used to define modular arithmetic.
We then form the type of integers modulo 2:[1] The operations on integers, +, - can be proven to be well-defined on the new quotient type.
However, unlike with setoids, many type theories may require a formal proof that any functions defined on quotient types are well-defined.
Just as product types and sum types are analogous to the cartesian product and disjoint union of abstract algebraic structures, quotient types reflect the concept of set-theoretic quotients, sets whose elements are partitioned into equivalence classes by a given equivalence relation on the set.