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

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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

nLab > Latest Changes: setoid

Bottom of Page

1 to 14 of 14

  1.  
    • CommentRowNumber1.
    • CommentAuthorMike Shulman
    • CommentTimeApr 12th 2021

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

    v1, current

  2. past few edits I added more information about setoids

    anonymous

    v8, current

  3. past few edits I added a section on extensional functions, the section on extensional functions probably should be made into its own article.

    anonymous

    v47, current

    • CommentRowNumber4.
    • CommentAuthorRodMcGuire
    • CommentTimeApr 27th 2022

    v8, current

    v47, current

    Why are you creating so many versions? The preview button does work and you could have added just 2 versions

  5. added section on the proper definition of setoid, with a pseudo-equivalence relation

    Anonymous

    diff, v13, current

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeFeb 7th 2023
    • (edited Feb 7th 2023)

    am giving this poor entry its first references:

    The notion goes back to the definition of sets in constructive mathematics according to

    Review and formalization in type theory:

    • Gilles Barthe, Venanzio Capretta, Olivier Pons, Setoids in type theory, Journal of Functional Programming 13 2 (2003) 261-293 [doi:10.1017/S0956796802004501]

    diff, v27, current

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeFeb 9th 2023

    added pointer to the original:

    diff, v28, current

    • CommentRowNumber8.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 6th 2023

    Re #5,

    Anonymous, if you’re there: can you verify who says it should be pseudo-equivalence relations instead of just equivalence relations?

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeJun 6th 2023

    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 SetoidSetoid to be the ex/lex completion of SetSet.

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

    diff, v29, current

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

    • CommentRowNumber11.
    • CommentAuthorHurkyl
    • CommentTimeJun 17th 2023

    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 SetoidSetoid is the essential image of SetSet in CatCat. 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.

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeJun 17th 2023

    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.

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeJun 17th 2023

    I have added a mentioning of groupoids up front (here)

    and the warning about differing terminology here (thereby essentily moving to here a paragraph that used to be at equivalence relation, as announced there)

    diff, v31, current

  14. I have moved everything specifically about pseudo-equivalence relations from setoid into its own article at pseudo-equivalence relation. Mike Shulman’s originally intended setoid to be a disambiguation page, as he writes here.

    diff, v32, current

1 to 14 of 14

  1.