Editing Setoid (section)

{{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).