Not signed in (Sign In)

# 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

• Sign in using OpenID

## Site Tag Cloud

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

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

• CommentRowNumber2.
• CommentAuthorGuest
• CommentTime5 days ago

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?

• CommentRowNumber3.
• CommentAuthorGuest
• CommentTime5 days ago

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

• CommentRowNumber4.
• CommentAuthorGuest
• CommentTime5 days ago

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.

• CommentRowNumber5.
• CommentAuthorGuest
• CommentTime5 days ago

@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$.

• CommentRowNumber6.
• CommentAuthorGuest
• CommentTime5 days ago

@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”.

• CommentRowNumber7.
• CommentAuthorGuest
• CommentTime5 days ago

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.

• CommentRowNumber8.
• CommentAuthorGuest
• CommentTime5 days ago

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

• CommentRowNumber9.
• CommentAuthorGuest
• CommentTime5 days ago

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.

• CommentRowNumber10.
• CommentAuthorGuest
• CommentTime5 days ago

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.

Add your comments
• Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
• To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

• (Help)