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:


So start with some set 'T':

This set may already have some structure.

number set diagram
number relations diagram We can add extra structure in the form of relations between the elements:
This forms an equivilance relation which divides up the set (in this case into even and odd numbers). equivalence diagram
number fibre diagram Another way to look at this is as a map into set (as a fibre bundle).

For an Idris implementation of setoids see this github site


Oidification allows us to start with a single object and one (or more) arrows back to itself and generalise this to multiple objects. This new structure does not need to have arrows between every pair of objects but composition always exists and every object has an identity arrow.

Here the words 'object' and 'arrow' are used in the category theory sense as described on the page here.

Here are some examples:

  Single Object Multiple Objects


This imposes an external equivalence relation and internalises it.

The single object needs to have the reflexive relation, that is, be equal to itself.

An example would be a set with a set with a fixed number of elements.

Since the arrows are reflexive, symmetric and transitive this gives an equivalence relation.


This can be thought of as a weakening of a setiod. Instead of equivalences we have isomorphisms, that is the permutations show how objects are equal in multiple ways.

diagram diagram


Just to confuse things the naming conventions have changed here. Monoid has an 'oid' but this is the single object case. A Monoidoid is a category.

diagram diagram

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-2023 Martin John Baker - All rights reserved - privacy policy.