A *(term) from _(logic) for a type of *(abstraction) which takes a class of _(object)s according to some set of rules, providing new identities for objects that are identical <em>according to those rules</em>. This can also be restated to say that it takes one domain and an equivalence relation over it and produces a new domain from the collections of objects unified by the relation.

For example, if you want to describe the Rational numbers while knowing only the Integers, you can take:

"All answers to the equation <code>a * x = b</code> for any Integers <var>a</var> and <var>b</var>."

as describing <em>quotients</em> of Integers. This is, in fact, the origin of the term. The Rationals then are described as a domain of new (derived) objects, each of which is the set of equations which describe some equivalent or isomorphic concept. Specifically, the object we call "5/3" is an equivalence class of equations such as <code>x * 3 = 5</code>, <code>x * 6 = 10</code>, and so forth. So the quotienting is happening on pairs of Integers with this
equation, <code>(3,5)</code> , <code>(6,10)</code> , <code>(21,35)</code>, etc. Note that "5/3" as an object is an <em>abstraction</em>, and it is not universal that a quotienting suggests an immediate <em>implementation</em> as this one's name suggests a pair of Integers. A name like that for rationals is possible because there is a uniform concept of <em>normalization</em>: a single simplest representations with all other representations inductively derivable from it.

This is generally part of the mathematical tradition of forming inductive definitions from primitive axioms to describe higher-level concepts, but <strong>the point with Tunes is that we <em>don't</em> care which parts are core (<em>primitive</em>) and which are derived</strong>: we want to be able to implement some concepts and translate back and forth across an isomorphism as we need to. We deliberately do <em>not</em> want to care about implementation decisions after they are made.

<ul class="links">
<li>A _(formal but concise and informative overview| http://www.nuprl.org/documents/Construct_Formal_AT/title/subsection3_5_3.html) from the _(NuPrl) paper _("Formalizing Automata Theory I: Finite Automata"|http://www.nuprl.org/documents/Construct_Formal_AT/title/title.html) (_(".ps"|http://www.nuprl.org/documents/Construct_Formal_AT/title.ps)).
See also _(Quotient Types in Nuprl|http://www.cs.cornell.edu/Info/People/sfa/Nuprl/NuprlPrimitives/Xquotient_doc.html).
<li>A formal paper on _(quotient algebras| http://homepages.feis.herts.ac.uk/~jean/algspec/pr.html) of term-manipulation systems.
<li>A description of _(quotient structures| http://www.lri.fr/demons/theme2.en.html) in _(Coq).
</ul>
