# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeSep 12th 2012

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)

• CommentRowNumber2.
• CommentAuthorTobyBartels
• CommentTimeSep 12th 2012
• (edited Sep 12th 2012)

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.

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeSep 12th 2012

added a reference by Hofmann, seems to be the most detailed one.

• CommentRowNumber4.
• CommentAuthorMike Shulman
• CommentTimeSep 13th 2012

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.

• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeSep 13th 2012

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-$\infty$-category / internal $\infty$-category” thing.

• CommentRowNumber6.
• CommentAuthorTobyBartels
• CommentTimeSep 13th 2012

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.

• CommentRowNumber7.
• CommentAuthorTobyBartels
• CommentTimeSep 13th 2012

@ Mike: You may be thinking of setoid > history.

• CommentRowNumber8.
• CommentAuthorUrs
• CommentTimeSep 13th 2012
• (edited Sep 13th 2012)

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:

1. we can’t name the entry “set”, for it needs a qualifier,

2. 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.

3. 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”?

• CommentRowNumber9.
• CommentAuthorTobyBartels
• CommentTimeSep 13th 2012

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

• CommentRowNumber10.
• CommentAuthorUrs
• CommentTimeSep 13th 2012
• (edited Sep 13th 2012)

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!

• CommentRowNumber11.
• CommentAuthorMike Shulman
• CommentTimeSep 13th 2012

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.

• CommentRowNumber12.
• CommentAuthorTobyBartels
• CommentTimeSep 14th 2012

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

• CommentRowNumber13.
• CommentAuthorMike Shulman
• CommentTimeSep 14th 2012

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

• CommentRowNumber14.
• CommentAuthorUrs
• CommentTimeApr 3rd 2013

Added to the references the recent preprint by Palmgren-Wilander