View source for Setoid

{{Redirect|E-set|the technique in fertility medicine|e-SET}}
{{Use American English|date = March 2019}}
{{Short description|Mathematical construction of a set with an equivalence relation}}

In [[mathematics]], a '''setoid''' (''X'', ~) is a [[Set (mathematics)|set]] (or [[type (mathematics)|type]]) ''X'' equipped with an [[equivalence relation]] ~.  A setoid may also be called '''E-set''', '''[[Errett Bishop|Bishop]] set''', or '''extensional set'''.<ref>Alexandre Buisse, Peter Dybjer, [[doi:10.1016/j.entcs.2008.10.003|"The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories—an Intuitionistic Perspective"]], ''Electronic Notes in Theoretical Computer Science'' 218 (2008) 21–32.</ref>

Setoids are studied especially in [[proof theory]] and in [[type-theoretic]] [[foundations of mathematics]]. Often in mathematics, when one defines an equivalence relation on a set, one immediately forms the [[quotient set]] (turning equivalence into [[equality (mathematics)|equality]]). In contrast, setoids may be used when a difference between identity and equivalence must be maintained, often with an interpretation of [[intension]]al equality (the equality on the original set) and [[Extension (semantics)|extensional]] equality (the equivalence relation, or the equality on the quotient set).

==Proof theory==
In proof theory, particularly the proof theory of [[constructive mathematics]] based on the [[Curry–Howard correspondence]], one often identifies a mathematical [[Proposition (mathematics)|proposition]] with its set of [[proof (mathematics)|proof]]s (if any). A given proposition may have many proofs, of course; according to the principle of proof irrelevance, normally only the truth of the proposition matters, not which proof was used. However, the Curry–Howard correspondence can turn proofs into [[algorithm]]s, and differences between algorithms are often important. So proof theorists may prefer to identify a proposition with a ''setoid'' of proofs, considering proofs equivalent if they can be converted into one another through [[beta conversion]] or the like.

==Type theory==
In type-theoretic foundations of mathematics, setoids may be used in a type theory that lacks [[quotient type]]s to model general mathematical sets. For example, in [[Per Martin-Löf]]'s [[intuitionistic type theory]], there is no type of [[real number]]s, only a type of [[regular Cauchy sequence]]s of [[rational number]]s. To do [[real analysis]] in Martin-Löf's framework, therefore, one must work with a ''setoid'' of real numbers, the type of regular Cauchy sequences equipped with the usual notion of equivalence.  Predicates and functions of real numbers need to be defined for regular Cauchy sequences and proven to be compatible with the equivalence relation.  Typically (although it depends on the type theory used), the [[axiom of choice]] will hold for functions between types (intensional functions), but not for functions between setoids (extensional functions).{{clarify|date=October 2010}} The term "set" is variously used either as a synonym of "type" or as a synonym of "setoid".<ref>{{cite web|page=9|url=http://www.cs.chalmers.se/Cs/Research/Logic/TypesSS05/Extra/palmgren.pdf|title=Bishop's set theory}}</ref>

==Constructive mathematics==
In [[Constructivism (mathematics)|constructive mathematics]], one often takes a setoid with an [[apartness relation]] instead of an equivalence relation, called a '''constructive''' setoid. One sometimes also considers a '''partial''' setoid using a [[partial equivalence relation]] or partial apartness (see e.g. Barthe ''et al.'', section 1).

== See also ==

* [[Groupoid]]

==Notes==
<references/>

== References ==
*{{citation
 | last = Hofmann | first = Martin
 | contribution = A simple model for quotient types
 | doi = 10.1007/BFb0014055
 | location = Berlin
 | mr = 1477985
 | pages = 216–234
 | publisher = Springer
 | series = Lecture Notes in Comput. Sci.
 | title = Typed lambda calculi and applications (Edinburgh, 1995)
 | url = http://www.tcs.informatik.uni-muenchen.de/~mhofmann/tlca95.ps
 | volume = 902
 | year = 1995| isbn = 978-3-540-59048-4
 | citeseerx = 10.1.1.55.4629
 }}.
*{{citation
 | last1 = Barthe | first1 = Gilles
 | last2 = Capretta | first2 = Venanzio
 | last3 = Pons | first3 = Olivier
 | doi = 10.1017/S0956796802004501
 | issue = 2
 | journal = Journal of Functional Programming
 | mr = 1985376
 | pages = 261–293
 | title = Setoids in type theory
 | url = https://www.cs.ru.nl/~venanzio/publications/Setoids_JFP_2003.pdf
 | volume = 13
 | year = 2003| s2cid = 10069160
 }}.

==External links==

* [http://coq.inria.fr/library/Coq.Classes.SetoidClass.html Implementation of setoids] in [[Rocq]]
*{{nlab|id=setoid|title=Setoid}}
*{{nlab|id=Bishop+set|title=Bishop set}}

{{Mathematical logic}}
{{Set theory}}

[[Category:Abstract algebra]]
[[Category:Category theory]]
[[Category:Proof theory]]
[[Category:Type theory]]
[[Category:Equivalence (mathematics)]]