Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • 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

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeApr 12th 2021

    Added some more remarks about Bishop sets in type theory, including the fact that the relations used are usually untruncated.

    diff, v14, current

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeFeb 9th 2023

    added publication data and aRXiv link for:

    diff, v16, current

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeFeb 9th 2023

    added publication data to:

    • Thierry Coquand, Arnaud Spiwack, section 3 of: Towards constructive homological algebra in type theory, in: Towards Mechanized Mathematical Assistants. MKM Calculemus 2007, Lecture Notes in Computer Science 4573 Springer (2007) [doi, pdf]

    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.

    diff, v16, current