Maths - Setoid


In mathematics, a setoid (X, ~) is a set (or type) X equipped with an equivalence relation ~.

Often in mathematics, when one defines an equivalence relation on a set, one immediately forms the quotient set (turning equivalence into equality). In contrast, setoids may be used when a difference between identity and equivalence must be maintained, often with an interpretation of intensional equality (the equality on the original set) and extensional equality (the equivalence relation, or the equality on the quotient set). - From Wiki

One way to define a setoid is define a tuple consisting of:

For an Idris implementation of setoids see this github site

Relationship to Groupoid

  Group Definition Equivalence Definition
Identity a = a•Id = Id •a



Reverse a•inv(a) = inv(a)•a = Id


if a~b then b~a

Associatively a•(b•c) = (a•b)•c


if a~b and b~c then a~c

Groupoid is explained on this page.

A central idea in the definition of setoid is not to insist upon equality between proof objects.

Extensionality of functions

if f(x) = g(x) for all x

then f = g

Example - consider the two functions f and g mapping from and to natural numbers, defined as follows:

These functions are extensionally equal; given the same input, both functions always produce the same value. But the definitions of the functions are not equal, and in that intensional sense the functions are not the same.

Functions between Setoids

Extensional Functions between Setoids

A function between setoids is a function between the underlying types (sets) together with a proof of extensionality:

A function |f| : |X|->|Y| is extensional, with respect to the equalities of X and Y,if there is a term of type:

f ~X=>Y g: Π|x|,|x'|:|X| x ~X x' -> |f|(x) ~Y |f|(y)

The bars, as in |x|, indicate x is an element of the underlying type. This distinction will usually be dropped if extensionality applies.




metadata block
see also:

This Site

Other Sites

Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

cover Modern Graph Theory (Graduate Texts in Mathematics, 184)

Terminology and Notation

Specific to this page here:


This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2021 Martin John Baker - All rights reserved - privacy policy.