In mathematics, a setoid (X, ~) is a set (or type) X equipped with an equivalence relation ~. A setoid may also be called E-set, Bishop set, or extensional set. 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). 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).
| Property |
Value |
| dbo:abstract |
In mathematics, a setoid (X, ~) is a set (or type) X equipped with an equivalence relation ~. A setoid may also be called E-set, Bishop set, or extensional set. 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). 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). (en) |
| dbo:wikiPageExternalLink |
https://www.cs.ru.nl/~venanzio/publications/Setoids_JFP_2003.pdf http://coq.inria.fr/library/Coq.Classes.SetoidClass.html http://www.tcs.informatik.uni-muenchen.de/~mhofmann/tlca95.ps |
| dbo:wikiPageID |
769434 (xsd:integer) |
| dbo:wikiPageLength |
4921 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID |
1102761185 (xsd:integer) |
| dbo:wikiPageWikiLink |
dbr:Algorithm dbr:Apartness_relation dbr:Per_Martin-Löf dbr:Intension dbr:Intuitionistic_type_theory dbr:Real_analysis dbr:Coq dbc:Proof_theory dbr:Mathematics dbr:Quotient_set dbr:Quotient_type dbr:Equality_(mathematics) dbr:Partial_equivalence_relation dbr:Curry–Howard_correspondence dbr:Equivalence_relation dbr:Errett_Bishop dbr:Foundations_of_mathematics dbr:Proof_theory dbc:Category_theory dbc:Abstract_algebra dbc:Type_theory dbr:Axiom_of_choice dbr:Constructivism_(mathematics) dbr:Groupoid dbr:Rational_number dbr:Real_number dbr:Set_(mathematics) dbr:Extension_(semantics) dbr:Proof_(mathematics) dbr:Proposition_(mathematics) dbr:Regular_Cauchy_sequence dbr:Constructive_mathematics dbr:Beta_conversion dbr:Type-theoretic dbr:Type_(mathematics) dbr:Proof_irrelevance |
| dbp:id |
Bishop+set (en) setoid (en) |
| dbp:title |
Bishop set (en) Setoid (en) |
| dbp:wikiPageUsesTemplate |
dbt:Citation dbt:Clarify dbt:Nlab dbt:Redirect dbt:Short_description dbt:Use_American_English |
| dct:subject |
dbc:Proof_theory dbc:Category_theory dbc:Abstract_algebra dbc:Type_theory |
| rdfs:comment |
In mathematics, a setoid (X, ~) is a set (or type) X equipped with an equivalence relation ~. A setoid may also be called E-set, Bishop set, or extensional set. 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). 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). (en) |
| rdfs:label |
Setoid (en) |
| owl:sameAs |
freebase:Setoid wikidata:Setoid https://global.dbpedia.org/id/4v2E3 |
| prov:wasDerivedFrom |
wikipedia-en:Setoid?oldid=1102761185&ns=0 |
| foaf:isPrimaryTopicOf |
wikipedia-en:Setoid |
| is dbo:wikiPageRedirects of |
dbr:Bishop_set dbr:E-Set dbr:E-set dbr:Extensional_set |
| is dbo:wikiPageWikiLink of |
dbr:Apartness_relation dbr:Intuitionistic_type_theory dbr:Quotient_type dbr:Constructive_set_theory dbr:Partial_equivalence_relation dbr:Equivalence_relation dbr:Partition_of_a_set dbr:Groupoid dbr:Set_(abstract_data_type) dbr:Extensionality dbr:Bishop_set dbr:E-Set dbr:E-set dbr:Extensional_set |
| is foaf:primaryTopic of |
wikipedia-en:Setoid |