Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

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

1. • CommentRowNumber1.
   • CommentAuthorMadeleine Birchfield
   • CommentTimeSep 20th 2022
   • (edited Sep 20th 2022)
   • PermaLink
   Author: Madeleine Birchfield
   Format: MarkdownItexI mentioned the recently created [[quotient setoid]] article on the HoTT summer school discord and Amelia Liao says that > this is incorrect actually > setoids do not have truncated equivalence relations > like, very explicitly the equivalence relation of a setoid should be valued in sets; that's what you get when you take the ex/lex completion of [the category of junk you have laying around] This implies that there is a distinction between [[setoids]] and a type with a symmetric preorder in homotopy type theory, and that much of the material on the nLab which talks about 'setoids' (such as in [[univalent setoid]], [[enriched setoid]], [[types and logic - table]], et cetera) should actually be about 'symmetric preorders'. Related is the notion of [[Bishop set]], which is a symmetric preorder without a propositional truncation condition on the hom-types at all. As a result, a Bishop set could probably also be called a "wild symmetric preorder", in the same sense that a [[wild category]] is a category without a set-truncation condition on the hom-types. However, the article on Bishop sets has the following sentence: (If the type theory has identity types, one could demand that $R$ consist of h-propositions, but at least historically this is not often done.)

   I mentioned the recently created quotient setoid article on the HoTT summer school discord and Amelia Liao says that

   this is incorrect actually

   setoids do not have truncated equivalence relations

   like, very explicitly the equivalence relation of a setoid should be valued in sets; that’s what you get when you take the ex/lex completion of [the category of junk you have laying around]

   This implies that there is a distinction between setoids and a type with a symmetric preorder in homotopy type theory, and that much of the material on the nLab which talks about ’setoids’ (such as in univalent setoid, enriched setoid, types and logic - table, et cetera) should actually be about ’symmetric preorders’.

   Related is the notion of Bishop set, which is a symmetric preorder without a propositional truncation condition on the hom-types at all. As a result, a Bishop set could probably also be called a “wild symmetric preorder”, in the same sense that a wild category is a category without a set-truncation condition on the hom-types. However, the article on Bishop sets has the following sentence: (If the type theory has identity types, one could demand that $R$ consist of h-propositions, but at least historically this is not often done.)

2. • CommentRowNumber2.
   • CommentAuthorGuest
   • CommentTimeSep 20th 2022
   • PermaLink
   Author: Guest
   Format: MarkdownItexThe article on Bishop sets states that > Frequently, the type theories used for this purpose do not even have a separate notion of “relation” or “proposition”, and thus the untruncated propositions as types interpretation is used for the equivalence relations in a Bishop set. That is, one has a type $X:Type$ of elements and a type family $R:X\to X \to Type$ with witnesses that it is “reflexive, symmetric, and transitive”, but nothing prevents $R(x,y)$ from having more than one element. (If the type theory has identity types, one could demand that $R$ consist of h-propositions, but at least historically this is not often done.) This means that categorically, the Bishop sets are most like the ex/lex completion of the category of types — although the morphisms in the ex/lex completion are defined as a quotient in the ambient set theory, whereas the morphisms between Bishop sets simply form another Bishop set. Assuming the traditional definition of a Bishop set (no truncations), in the context of homotopy type theory, * What is a Bishop set in the simplicial set model of homotopy type theory? * In homotopy type theory, types represent infinity-groupoids, and so the "category" of types is actually an infinity-category. Do ex/lex completions exist in the context of infinity-category theory? * If ex/lex completions exist, then do the Bishop sets behave like the ex/lex completion of the infinity-category of infinity-groupoids?

   The article on Bishop sets states that

   Frequently, the type theories used for this purpose do not even have a separate notion of “relation” or “proposition”, and thus the untruncated propositions as types interpretation is used for the equivalence relations in a Bishop set. That is, one has a type $X:Type$ of elements and a type family $R:X\to X \to Type$ with witnesses that it is “reflexive, symmetric, and transitive”, but nothing prevents $R(x,y)$ from having more than one element. (If the type theory has identity types, one could demand that $R$ consist of h-propositions, but at least historically this is not often done.) This means that categorically, the Bishop sets are most like the ex/lex completion of the category of types — although the morphisms in the ex/lex completion are defined as a quotient in the ambient set theory, whereas the morphisms between Bishop sets simply form another Bishop set.

   Assuming the traditional definition of a Bishop set (no truncations), in the context of homotopy type theory,

   • What is a Bishop set in the simplicial set model of homotopy type theory?

   • In homotopy type theory, types represent infinity-groupoids, and so the “category” of types is actually an infinity-category. Do ex/lex completions exist in the context of infinity-category theory?

   • If ex/lex completions exist, then do the Bishop sets behave like the ex/lex completion of the infinity-category of infinity-groupoids?

3. • CommentRowNumber3.
   • CommentAuthorGuest
   • CommentTimeSep 20th 2022
   • PermaLink
   Author: Guest
   Format: MarkdownItexI'd say that one should in general distinguish between a type theoretic concept (Bishop set) and its semantics in certain models (i.e. setoids).

   I’d say that one should in general distinguish between a type theoretic concept (Bishop set) and its semantics in certain models (i.e. setoids).

4. • CommentRowNumber4.
   • CommentAuthorGuest
   • CommentTimeSep 20th 2022
   • PermaLink
   Author: Guest
   Format: MarkdownItexWell I've created the article [[sets in homotopy type theory]] which addresses the distinction between the various notions of sets in homotopy type theory.

   Well I’ve created the article sets in homotopy type theory which addresses the distinction between the various notions of sets in homotopy type theory.

5. • CommentRowNumber5.
   • CommentAuthorGuest
   • CommentTimeSep 20th 2022
   • PermaLink
   Author: Guest
   Format: MarkdownItex@2 Bishop sets were usually formulated in a set-level MLTT for which [[uniqueness of identity proofs]] is usually assumed. The proper definition in HoTT of a Bishop set would require set-truncations in both the object type and the hom-types, and would basically be a strict [[magmoid]] with functions $\dagger_{a, b}:Hom(a, b) \to Hom(b, a)$ for all objects $a:A$ and $b:A$.

   @2

   Bishop sets were usually formulated in a set-level MLTT for which uniqueness of identity proofs is usually assumed. The proper definition in HoTT of a Bishop set would require set-truncations in both the object type and the hom-types, and would basically be a strict magmoid with functions $\dagger_{a, b}:Hom(a, b) \to Hom(b, a)$ for all objects $a:A$ and $b:A$.

6. • CommentRowNumber6.
   • CommentAuthorGuest
   • CommentTimeSep 20th 2022
   • PermaLink
   Author: Guest
   Format: MarkdownItex@3 In fact, it's the other way around. Bishop sets are the notion used elsewhere (i.e. in material and structural constructive set theories lacking quotients) and it is the formalization in type theory that is usually called "setoid".

   @3

   In fact, it’s the other way around. Bishop sets are the notion used elsewhere (i.e. in material and structural constructive set theories lacking quotients) and it is the formalization in type theory that is usually called “setoid”.

7. • CommentRowNumber7.
   • CommentAuthorGuest
   • CommentTimeSep 20th 2022
   • PermaLink
   Author: Guest
   Format: MarkdownItexThe guest at 5 wrote > Bishop sets were usually formulated in a set-level MLTT for which uniqueness of identity proofs is usually assumed. The proper definition in HoTT of a Bishop set would require set-truncations in both the object type and the hom-types, and would basically be a strict magmoid with functions $\dagger_{a, b}:Hom(a, b) \to Hom(b, a)$ for all objects $a:A$ and $b:A$. This is actually where the notion of "Bishop set"/"setoid" bifurcates into 4 different notions in HoTT, depending on how one interprets the definition from strictness to univalence. We could have Bishop sets where the base type is set-truncated, where the base type isn't truncated but each relation-type is set-truncated, where both are set-truncated, and where neither are set-truncated. A similar thing happens with the definition of category in HoTT, resulting in [[wild categories]], [[precategory]], [[strict category]], and set-truncated wild categories.

   The guest at 5 wrote

   Bishop sets were usually formulated in a set-level MLTT for which uniqueness of identity proofs is usually assumed. The proper definition in HoTT of a Bishop set would require set-truncations in both the object type and the hom-types, and would basically be a strict magmoid with functions $\dagger_{a, b}:Hom(a, b) \to Hom(b, a)$ for all objects $a:A$ and $b:A$.

   This is actually where the notion of “Bishop set”/”setoid” bifurcates into 4 different notions in HoTT, depending on how one interprets the definition from strictness to univalence. We could have Bishop sets where the base type is set-truncated, where the base type isn’t truncated but each relation-type is set-truncated, where both are set-truncated, and where neither are set-truncated.

   A similar thing happens with the definition of category in HoTT, resulting in wild categories, precategory, strict category, and set-truncated wild categories.

8. • CommentRowNumber8.
   • CommentAuthorGuest
   • CommentTimeSep 20th 2022
   • PermaLink
   Author: Guest
   Format: MarkdownItex@7 I would agree with you if it weren't for all the prior results from category theory stating that Bishop sets form a [[predicative topos]] and/or are the [[ex/lex completion]] of the category of types, all of which imply that Bishop sets are 0-truncated. Otherwise one would be talking about the 2-category of Bishop sets or the (infinity, 1)-category of Bishop sets rather than the category of Bishop sets.

   @7

   I would agree with you if it weren’t for all the prior results from category theory stating that Bishop sets form a predicative topos and/or are the ex/lex completion of the category of types, all of which imply that Bishop sets are 0-truncated. Otherwise one would be talking about the 2-category of Bishop sets or the (infinity, 1)-category of Bishop sets rather than the category of Bishop sets.

9. • CommentRowNumber9.
   • CommentAuthorGuest
   • CommentTimeSep 20th 2022
   • PermaLink
   Author: Guest
   Format: MarkdownItexThe guest at 8 said > I would agree with you if it weren’t for all the prior results from category theory stating that Bishop sets form a predicative topos and/or are the ex/lex completion of the category of types, all of which imply that Bishop sets are 0-truncated. Otherwise one would be talking about the 2-category of Bishop sets or the (infinity, 1)-category of Bishop sets rather than the category of Bishop sets. However, in any set theory or set-level type theory categories are sets as well, so that isn't really relevant when translating to a foundations where [[UIP]] or [[axiom K]] isn't a theorem or axiom. One could easily talk about Bishop presets and strict Bishop sets in the same way one does monoidal precategories and strict monoidal categories.

   The guest at 8 said

   I would agree with you if it weren’t for all the prior results from category theory stating that Bishop sets form a predicative topos and/or are the ex/lex completion of the category of types, all of which imply that Bishop sets are 0-truncated. Otherwise one would be talking about the 2-category of Bishop sets or the (infinity, 1)-category of Bishop sets rather than the category of Bishop sets.

   However, in any set theory or set-level type theory categories are sets as well, so that isn’t really relevant when translating to a foundations where UIP or axiom K isn’t a theorem or axiom. One could easily talk about Bishop presets and strict Bishop sets in the same way one does monoidal precategories and strict monoidal categories.

10. • CommentRowNumber10.
    • CommentAuthorGuest
    • CommentTimeSep 20th 2022
    • PermaLink
    Author: Guest
    Format: MarkdownItexErrett Bishop wrote > To define a set we prescribe, at least implicitly, what we (the constructing intelligence) must do in order to construct an element of the set, and what we must do to show that two elements are equal” Type theorists have historically been using the term "equivalence relation" wrong in the definition of Bishop set. Following Errett Bishop, in order to show that two elements are equal, it is not enough to exhibit a witness of an "equivalence relation types" $a =_A b$. One also has to show that any two witnesses of such an equivalence relation type $c, d:a =_A b$ are equal, which means that one would also have to construct the equivalence relation type $c =_{a =_A b} d$ and exhibit a witness of that equivalence relation type. But then one needs to show that any two witnesses of that equivalence relation type are equal to each other, and so those equivalence types in turn would need to have their own equivalence relation types $e =_{c =_{a =_A b} d} f$ for $e, f:c =_{a =_A b} d$, and so on. This leads to an infinite tower of equivalence relation types.

    Errett Bishop wrote

    To define a set we prescribe, at least implicitly, what we (the constructing intelligence) must do in order to construct an element of the set, and what we must do to show that two elements are equal”

    Type theorists have historically been using the term “equivalence relation” wrong in the definition of Bishop set.

    Following Errett Bishop, in order to show that two elements are equal, it is not enough to exhibit a witness of an “equivalence relation types” $a =_A b$. One also has to show that any two witnesses of such an equivalence relation type $c, d:a =_A b$ are equal, which means that one would also have to construct the equivalence relation type $c =_{a =_A b} d$ and exhibit a witness of that equivalence relation type. But then one needs to show that any two witnesses of that equivalence relation type are equal to each other, and so those equivalence types in turn would need to have their own equivalence relation types $e =_{c =_{a =_A b} d} f$ for $e, f:c =_{a =_A b} d$, and so on.

    This leads to an infinite tower of equivalence relation types.

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeSep 26th 2022
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexRe 10, while I love that description of what it means to define a "set" (which then of course actually means a homotopy type) -- indeed, it's the basic idea of higher observational type theory -- I see no reason to think that it's what Bishop meant.

    Re 10, while I love that description of what it means to define a “set” (which then of course actually means a homotopy type) – indeed, it’s the basic idea of higher observational type theory – I see no reason to think that it’s what Bishop meant.

12. • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeSep 26th 2022
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexAlso, can all you Guests PLEASE sign your comments with distinguishable pseudonyms?!

    Also, can all you Guests PLEASE sign your comments with distinguishable pseudonyms?!