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 Bishop set to go with the discussion in another thread here
(I have tried to cross-link this to the relant entries, but maybe Toby should look over this. I suppose some further existing nLab discussion of Bishop’s work could be cross linked here)
I think that the page should probably simply be setoid. I don’t have to time to expand it now. But I did the redirects.
added a reference by Hofmann, seems to be the most detailed one.
I could have sworn that we already had a page called setoid. I guess I’m just remembering that it used to redirect to equivalence relation.
Yes, that’s how it was.
I am not a fan of the word “setoid”. I know that they all use it. And I find it kind of remarkable how Bishop’s idea turned out to be so good after all. So I like “Bishop set”.
There is even some resonance between his “preset / set” and the “internal pre--category / internal -category” thing.
One problem with ‘Bishop set’ is that nobody uses the word. And since the proper word is just ‘set’, I’m not sure why anybody would. Not to justify ‘setoid’ either, but at least it’s used.
@ Mike: You may be thinking of setoid > history.
One problem with ‘Bishop set’ is that nobody uses the word.
It’s still okay that the entry is named this way though, with “setoid” redirecting to it. Agreed?
For, let’s see:
we can’t name the entry “set”, for it needs a qualifier,
we can*t name it “setoid” (at least I can’t) for that is a confused term that violates the fundamental -oid-convention. Really a _setoid_ is a _set with many objects_ – which is a set. Which brings us back to 1. Whoever invented the terminology “setoid” was trying to say “0-groupoid” and failed.
but if you find “Bishop” an improper qualifier, we can look for other ones: how about “constructive set” or “set in constructive mathematics” or “set in predicative mathematics”?
Whoever invented the terminology “setoid” was trying to say “0-groupoid” and failed.
I don’t think that they were trying to say anything in analogy with ‘groupoid’. The suffix ‘oid’ is a generic one for a similar but different thing. Faced with a poor concept of ‘set’ and seeing how to fix it, they decided to use a new word. (I have no idea who this was, by the way.)
I really don’t like the options in (3), precisely because it is in constructive and predicative mathematics that one encounters the term ‘setoid’ (and sees the word ‘set’ being used, in effect, incorrectly).
But to come back to the staus quo: is it so bad if the entry is named “Bishop set” and you refer to it by “setoid”?
I find “Bishop set” is a perfect term in the context of a wiki where we need accurate disambiguation of many different notions of the same general name, which is different from what one needs in a specified context as in a type-theory textbook.
The entry is about that particular version of “set” that was proposed be Errett Bishop. And which in contexts where people know what they mean is called a “setoid”.
Seems okay to me.
But: if you feel you need to rename the entry, please do!
I don’t really agree that setoids are “the notion of set proposed by Errett Bishop.” IIRC, Bishop was not about any sort of formalization. Speaking of setoids in a preset theory or type theory might be motivated by Bishop’s philosophy, but is not exactly the same thing. Since the entry is largely about its formal expression rather than the philosophy, I think it is more appropriate to use a term which means that, and ’setoid’ is the absolutely standard word used by everyone who talks about these things.
The entry is a bit more about Bishop’s philosophy than I’d expect from an entry called setoid, but certainly the last half would fit better there than at Bishop set.
I don’t think, Urs, that you have any obligation to change anything. But Mike or I might. I will tomorrow, if I have time.
Actually, I might edit setoid > history to be something that I would like to call setoid, and then see if that should be merged with Bishop set, or maybe even kept separate with the formal stuff in an appropriate place. (Or perhaps Mike will do something else first.)
Toby, your plan sounds good to me. Having separate pages Bishop set about philosophy and setoid about formal things seems reasonable. I probably won’t have time to do much nLab-editing for several days (about to go move to Princeton for a year!).
Added to the references the recent preprint by Palmgren-Wilander
added publication data and aRXiv link for:
added publication data to:
This is the only one of the references where I see the term “Bishop set” actually being used – and it seems to be introduced there.(?)
I don’t see how their use of “Bishop set” is not entirely synonymous with “setoid”(?) and I wonder if the two entries should not simply be merged.
Somewhat surprisingly, Coquand and Spiwack don’t cite Hofmann 1995 where “setoid” seems to be introduced, so it’s hard to know what was going on there.
1 to 17 of 17