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.
1 to 10 of 10
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.)
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?
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).
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.
@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$.
@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”.
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.
@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.
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.
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.
1 to 10 of 10