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.
I do not feel sure enough about HTT to do this but the term homotopy type seems to be ambiguous as there is the traditional meaning of an equivalence class under homotopy equivalence or weak homotopy equivalence, but also the analogue in HTT of ’type’ in the logical sense. Would a mention of this ambiguity be a good thing to add somewhere, if so where?
All along I think people (Mike comes to mind especially) have delighted in the ambiguity, that HTT can be read either as “(homotopy type) theory” or “homotopy (type theory)”. That sort of thing should be mentioned somewhere in the Lab (if it hasn’t already), but maybe just to point out the serendipity.
Yes, as Todd says, there is not actually an ambiguity in the sense of “homotopy type” in logic and the traditional sense: the traditional sense is a special case or rather a model for the logical sense. (I thought I once added a sentence to that effect to the entry, but maybe I didn’t).
There is however an ambiguity within either of these senses itself: do we insist that “homotopy type” is the equivalence class or do we rather refer to the equivalence here as saying “ and are equivalent homotopy types”, both of them being actual objects in an -category, not equivalence classes.
I think this latter use us much more natural and useful, and subsumes the former sense, if really desired. So even if this maybe not be 100% in line with traditional use of the term, I’d strongly suggest that we don’t insist that “homotopy type” refers to an equivalence class, but instead agree that it refers to a representaitve of that equivalence class.
we don’t insist that “homotopy type” refers to an equivalence class,
I would happily go along with that and there is a similar use and ambiguity with ’n-type’. ’An object is an n-type’ is taken to mean that it has trivial homotopy groups above dimension n (and of course there are lots of other terms that are used for related or equivalent concepts), but ’an n-type is an equivalence class of objects under the relation of n-equivalence’.
there is not actually an ambiguity in the sense of “homotopy type” in logic and the traditional sense: the traditional sense is a special case or rather a model for the logical sense
I would argue that there is an ambiguity if we use the same word for two things, one of which is a model of the other. A model is not the same as a special case. Perhaps the place for a disambiguation would be homotopy type?
Hm. If an is a , then we don’t usually dismabiguate entries for and . We say that one is a spcial case of the other.
Here we should say: a homotopy type in the traditional sense is the special case of a homotopy type in the general sense for the case that the ambient context is the -category of topological spaces simplically localized at the weak homotopy equivalences.
It did already say this, mostly. I added a further sentence to maybe make it clearer.
Here is what I have now:
Traditionally, a homotopy type is a topological space regarded up to weak homotopy equivalence, (although this may sometimes be reeferred to as its weak homotopy type, (see below)). Formally this may be taken to mean the object that represents in the standard homotopy category Ho(Top), or, better, in the (∞,1)-category ∞Grpd , the simplicial localization of the category Top at the weak homotopy equivalences, of which is the decategorification. As such, topological spaces regarded as homotopy types are equivalently ∞-groupoids (see at homotopy hypothesis for more on this).
More generally, then, we may think of every object in any (∞,1)-category or at least every (∞,1)-topos as being a homotopy type in the context . For instance if is an (∞,1)-category of (∞,1)-sheaves/of ∞-stacks over some (∞,1)-site , then an object of may be thought of as a homotopy type over . For the special case that , this reproduces the traditional notion.
If the (∞,1)-category here is at least a locally cartesian closed (∞,1)-category then its internal language is a model for the formal logic called homotopy type theory. The types of this theory may therefore also be called homotopy types, abstractly, and the concrete homotopy types in the sense of objects of are then the categorical semantics of these abstract homotopy types.
That looks good to me. Thanks.
a homotopy type in the traditional sense is the special case of a homotopy type in the general sense for the case that the ambient context is the ∞-category of topological spaces simplically localized at the weak homotopy equivalences.
I don’t agree. I would say that a homotopy type in the traditional sense is the special case of a model of a homotopy type in the type-theoretic sense, where we consider semantics in the (∞,1)-category of topological spaces localized at whes.
Well, the text mentions this just a few lines below.
I’d edit further. But the Lab doesn’t react at the moment. Maybe you’ll have a second to adjust it to your liking later.
But I am thinking that if you want to be very pedantic about this, changes in wording are required in a bunch of related entries.
Wait a moment, Mike. Could it be that you are commenting on a version that is already overwritten? Please check again the current version.
Hmm, okay, I guess you are introducing a third meaning of “homotopy type”, namely “object of an -topos”, which bridges the other two. I’m not sure if I like that; it seems to me like using the word “set” to mean “object of a 1-topos”.
it seems to me like using the word “set” to mean “object of a 1-topos”.
Indeed. As in “variable sets” or “h-Set” . I’d say.
hSet has exactly the same problems as ’homotopy type’, so you can’t invoke it as an argument. ’Variable set’ is a weird nonstandard term of Lawvere, but even if it were standard, there is an important adjective on it that you can’t ignore.
Hm, not sure what to say. I am a bit surprised that you are objecting to call an object of an -topos a homotopy type. I thought that’s the whole fun of it that we are entirely entitled to do that. And speaking of cohesive homotopy type and so forth. I’d find it sad to add lots of qulifications to these terms only to amplify a difference of which the whole point is that we may ignore it.
But let me turn this around: what would be your suggestion? So we have
in the internal language: homotopy type
in the canonical model: homotopy type
in the generic model: what should go here?
We are entitled to do that only when we are working in the internal language. I would have thought that after all the trouble you had understanding type theory once upon a time, you’d be more sympathetic to people who still get confused by things like the internal/external distinctions!
in the generic model: object. Or, (homotopy) sheaf.
I certainly see what you mean. But by historical accident in one does say “homotopy type” even if not in the internal language.
Would you be happy with sheaf of homotopy types? Or variable homotopy type?
Actually concerning Lawvere’s variable: I’d find something like “structured” much more descriptive. Because while we write down sheaves/-stacks as “variable” sets/homotopy types, what it actually amounts to is that we equip them with some kind of structure. In some sense.
But by historical accident in one does say “homotopy type” even if not in the internal language.
I would argue that in that case, the internal and external languages basically coincide – that is, is a well-pointed -topos. So the historical accident is entirely consistent. (It’s also consistent with saying “set” when internal to a 1-topos, and also externally for the well-pointed 1-topos .)
I’m happy with “sheaf of homotopy types” or “variable homotopy type” in general, and with “cohesive homotopy type” in the case that the ambient -topos is cohesive. I feel like the problem with “structured” is that it’s too general: there are lots of categories of structured homotopy types that aren’t -toposes.
I did some editing at homotopy type, see what you think.
Very nice, thanks!
1 to 22 of 22