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.
It’s not clear to me that a “setoid” in HoTT should refer to a structure built out of h-sets. At first thought, it makes more sense to me for a “setoid” in HoTT to mean the same thing that it does in plain intensional MLTT, namely a structure built out of arbitrary types.
I find the organization and goals of this page a bit confusing. It starts out by talking about a lot of different foundations, but the page title and the definitions section seem to be specific to homotopy type theory. In homotopy type theory (not just cubical type theory), h-sets are the correct notion of “set”, so it’s misleading to put all of these others on a common footing. If the goal is mainly historical and comparative, perhaps the page should be called “set-like structures in homotopy type theory”?
Also, it occurs to me that some more uniform terminology could be obtained by analogy to the case of categories:
If we specialize to groupoids, then in particular a (univalent) groupoid coincides with just a 1-type. So similarly, we could say:
That way each term would be precise, and we could avoid entirely the question of deciding what a “setoid” should mean in HoTT.
Mike Shulman writes
It’s not clear to me that a “setoid” in HoTT should refer to a structure built out of h-sets. At first thought, it makes more sense to me for a “setoid” in HoTT to mean the same thing that it does in plain intensional MLTT, namely a structure built out of arbitrary types.
But if we make setoids untruncated and their homs untruncated in homotopy type theory, then I don’t think the (infinity, 1)-category Setoid of setoids and setoid homomorphisms is the (1, 1)-categorical ex/lex completion of the (1,1)-category hSet anymore.
But if we make setoids untruncated and their homs untruncated in homotopy type theory, then I don’t think the (infinity, 1)-category Setoid of setoids and setoid homomorphisms is the (1, 1)-categorical ex/lex completion of the (1,1)-category hSet anymore.
Indeed, instead it should be the (1,1)-ex/lex completion of the -category of types.
I think I prefer my suggestion in #4, to resist saying “setoid” at all in HoTT. The problem is that in a set-level foundation, setoids must obviously consist of sets, while in plain intensional type theory, they must obviously consist of types, and there’s no a priori reason that in HoTT we should prefer one convention to the other. Fortunately, setoids also aren’t particularly useful in HoTT, so we don’t need to talk about them much.
Deleted
One could similarly define the following notions of setoids:
A wild setoid is the same as a wild set.
A presetoid is a wild setoid whose hom-types are h-sets. This is the same as a type with a pseudo-equivalence relation.
A strict setoid is a presetoid whose object type is also an h-set. These are the setoids talked about in set-level foundations.
A univalent setoid is a presetoid which satisfies the Rezk completion condition: equality of objects is the same as isomorphism of objects in the core of the presetoid, the maximal subpregroupoid of the presetoid.
Anonymous
A presetoid is a wild setoid whose hom-types are h-sets. This is the same as a type with a pseudo-equivalence relation.
We’ve just moved the problem from “setoid” to “pseudo-equivalence relation”. Is there any inherent reason for the dependent types of the pseudo-equivalence relation to be inherently 0-truncated in homotopy type theory?
Regarding setoids in intensional type theory/homotopy type theory, we should instead have -setoids, where refers to the truncation level on the object type and refers to the truncation level on the type-valued equivalence relation.
Yes, we can have all these things, but I don’t think they are important enough to give names and nLab pages too. It’s actually more confusing to proliferate unnecessary terminology. I think we should pare this page back to the bare minimum: all that it needs to do is clarify how pre-existing notions of “set” from other foundations are related to the correct notion of “set” in HoTT. It doesn’t need to introduce new notions like “presetoid” that no one is going to actually use (and I similarly think we should delete the page “presetoid”).
1 to 12 of 12