Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Created a stub / disambiguation page, to point to both equivalence relation and Bishop set and pseudo-equivalence relation (the latter currently redirecting to regular and exact completions).
v8, current
v47, current
Why are you creating so many versions? The preview button does work and you could have added just 2 versions
am giving this poor entry its first references:
The notion goes back to the definition of sets in constructive mathematics according to
Errett Bishop, Foundations of Constructive Analysis, Mcgraw-Hill (1967)
Errett Bishop, Douglas Bridges, p. 15 of: Constructive Analysis, Grundlehren der mathematischen Wissenschaften 279, Springer (1985) [doi:10.1007/978-3-642-61667-9]
Review and formalization in type theory:
added pointer to the original:
Re #5,
Anonymous, if you’re there: can you verify who says it should be pseudo-equivalence relations instead of just equivalence relations?
I am adding a list up-front here for which author says what.
Am deleting the following paragraph, since declaring “defaults” might work in a linear textbook but not in an open-world wiki adventure such as the nLab:
Sometimes, the term “setoid” is used in the mathematics literature for a set equipped with an equivalence relation, rather than a set equipped with a pseudo-equivalence relation. However, in the nLab we shall by default take setoids as those sets equipped with a pseudo-equivalence relation, which is required for the category $Setoid$ to be the ex/lex completion of $Set$.
To make up for this, I added a paragraph to the Idea section with some comments on why to choose one or the other definition (which could probably be expanded further).
The pseudo-equivalence relation link currently redirects to this article. Considering that the term “setoid” refers to two different kinds of objects in mathematics, equivalence relations and pseudo-equivalence relations, and the material about equivalence relations is over at the equivalence relation article rather than here, personally I would create a separate article specifically on pseudo-equivalence relations, move the material specifically about pseudo-equivalence relations from this article to that separate article, and leave this article on setoids as a disambiguation page linking to both equivalence relation and pseudo-equivalence relation.
Re #9, the page equivalence relation#a_categorical_view also contains this language.
In at least one corner of mathematics the notion of “setoid” is important through the fact $Setoid$ is the essential image of $Set$ in $Cat$. By which I mean I, personally, have basically only ever seen the word used for reasons that can be derived from this fact, and I had always assumed the etymology of the word is based on this – that the idea is setoids are groupoids that are equivalent to sets.
It would seem kind of weird to have this fact on the equivalence relation page, but maybe not. But I guess it’s already weird that this content isn’t on the setoid page either.
Re #9, the page equivalence relation#a_categorical_view also contains this language.
Thanks for pointing this out. I have edited, as now announced there.
I also find the entry setoid here leaves much room to be improved. If you have the energy to write something about setoids in the sense of equivalence relations, please do.
1 to 14 of 14