left and right euclidean;
An equivalence relation on a set is a binary relation on that is:
A setoid is a set equipped with an equivalence relation.
Equivalently, a setoid is a groupoid enriched over the cartesian monoidal category of truth values. Equivalently, a setoid is a groupoid that is 0-truncated. Then the equivalence relation on is a way of making into the set of objects of such a groupoid.
It may well be useful to consider several possible equivalence relations on a given set. When considering a single equivalence relation once and for all, however, it is common to take the quotient set and use that instead. As a groupoid, any setoid is equivalent to a set in this way (although in the absence of the axiom of choice, it is only a “weak” or ana-equivalence).
Setoids are still important in foundations of mathematics where quotient sets don't always exist and the above equivalence cannot be carried out. However, arguably this is a terminological mismatch, and such people should say ‘set’ where they say ‘setoid’ and something else (such as ‘preset’, ‘type’, or ‘completely presented set’) where they say ‘set’. (See page 9 of these lecture notes.)
A partial equivalence relation is a symmetric and transitive relation.