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.
Seems an odd choice ’anima’. But why would the plural be the same? Thought it was a feminine noun: here, so ’animae’.
I see here, p. 36:
If the objects of C are called widgets, then we call those of Ani(C) animated widgets, except that we abbreviate Ani(Set) to Ani and the term ‘animated set’ to anima (plural: anima).
Hmm.
I have to say that I am not animated by the terminology “anima”.
The ideosyncrasy reminds me of the fact that there still is no text that would serve as introducing/communicating homotopy theory to its neighbour fields (think of differential geometers, mathematical physicists, …).
“Anima” has an advantage of being a single short nonhyphenated word without special symbols that is already present in your spellchecker’s dictionary. Only “space” can compete with it, but a lot of people hate “space”.
Re #7: Not only we do not have a text that introduces modern homotopy theory to its neighbor fields, we also do not have a text that introduces modern homotopy theory to (future) homotopy theorists!
For example, the only published elementary introduction to simplicial sets is a short survey by Friedman. But it doesn’t go far.
Goerss and Jardine start by assuming the reader already mastered a textbook like Hatcher or tom Dieck.
Lurie’s Higher Topos Theory and Cisinski’s Higher Categories and Homotopical Algebra also assume a lot of background.
Lurie’s Kerodon could become a more accessible source one day.
There is the ancient survey article of Curtis on simplicial homotopy theory that does some nice stuff that is often not mentioned.
To return to this thread, I find the term ‘anima’ without any mental hook to attach it to an infinity groupoid.
The presumed mental hook (as indicated by Scholze) is that Beilinson referred to the process of introducing coherent homotopies (e.g., turning rings into simplicial rings, etc.) as “animating” them.
Only “space” can compete with it
What about “type”?
Re #11: Doesn’t “type” also refer to types in extensional type theory, which are not at all like homotopy types?
Those are just the 0-truncated ones. (-:
Looks right to me.
It is really annoying that homotopy theorists cannot settle on a single name, whether it is “space”, “type”, or “anima”.
I hope this changes soon and all but one terms die out. (I don’t even care that much which one wins.)
And we also need a shorter name for our profession. How about “homotopists” instead of “homotopy theorists”?
How about “homotopists” instead of “homotopy theorists”?
The short form should be “type theorists”.
(The years go by, and what once was the beginning of the bright future of a great new unifying idea is gradually becoming a faint memory of what could have been. Homotopy-Type-Theory, does anyone remember what this was about?)
Re #11, #17:
The meaning of “type” depends on the situation. Even if the meaning of “type” is always some special case of the homotopy types (and is that even suspected?), that’s still generally a different meaning from the entirety of homotopy types.
I like to think of myself as a type theorist, and I’m definitely not a homotopy theorist.
HoTT is great, but let’s not get carried away; type theory and abstract homotopy theory are not the same subject.
(What was the bright future? Why isn’t it happening? Is it too late?)
Re #18: One truly depressing aspect is that we still don’t know how to define (∞,1)-categories in homotopy type theory.
Yeah, and I think part of that is that you need coherence conditions at all dimensions, and nobody knows how to do that in most versions of HoTT. I think that problem is really interesting. I’m hoping there’s a sneaky way to do it already in Book HoTT, but it seems like most people think it can’t be done in Book HoTT. Given that, I’d have thought people would be trying to reach a consensus on what system to use instead, but it looks like they aren’t. They’re trying many different systems, and—it seems—not focusing on the ability to solve coherence problems.
I suppose I’m expressing my ignorance, but I thought the idea for (∞,1)-categories was via (infinity) precategories – functors such that is the type of -long strings of composable arrows. Then the (∞,1)-categories would be the one where the degeneracy is an equivalence with the subtype of invertible arrows.
Is the problem that we don’t know how to formalize Type-valued functors out of a 1-category? Or something else?
Re #21: If I understand it correctly, once we can define simplicial types (i.e., simplicial ∞-groupoids), then we know how to proceed to define (∞,1)-categories using Segal-type constructions.
However, a simplicial type is (or should be) a functor , and it is not at all clear how to encode all coherences here: for each we have a type , for each we have a map , for each and we have , and it seems like there is no easy way to encode all these in HoTT.
I have no idea what Urs is talking about in #17. It sounds like maybe the real world failed to live up to exaggerated expectations in some way?
Trying many different systems is part of the process of reaching a consensus on which is the best. Currently the most promising type theory for solving general coherence problems is some form of “2-level type theory”, but uptake of that has been slow, probably partly due to its arguably unaesthetic nature, partly to its not having been implemented directly in a proof assistant, partly due to hopes that something better will be found, and partly due to most people in the field having plenty of other problems to keep them busy that don’t require infinite coherence.
Re #7, #8: So what should a text (introducing/communicating homotopy theory to the masses) contain? If I knew what is supposed to be in it I might try to write it.
Hi Charles,
thanks for the message. Here some quick thoughts. Maybe to be followed up later when I am more awake.
Most importantly, it must Not start with talking about simplical categories or anything remotely like that. The audience in #7 has no idea what this means.
It’s not just that they don’t know the technical details (this audience is able to appreciate theory while glossing over details) but they have no idea what to make of such words at all.
The audience in #7 is typically used to seeing fairly sophisticated aspects of dg-homotopy theory, though not under that name.
These people often have religious feelings towards the equation . One could start by explaining how the simplicial identities generalize this homological “master equation”.
Hence besides briefly recalling elements of point-set topological homotopy, an introduction for them should probably motivate homotopy theory as the “non-abelian generalization” of homological algebra. Dold-Kan as the road to homotopy theory.
Derived categories might be an excellent point of contact, and motivating examples should be given in the context of complex-analytic/algebraic geometry.
(Yes, I think this audience may tend to have an easier time connecting to derived categories than to plain categories, much like many people think they know operads only in chain complexes. At least they all have heard of applications of derived categories, but will mostly never heard of a sensible application of a plain category.)
Just some quick thoughts. Maybe more later.
This entry was (and is) lacking references. I have now, at least, added pointer to:
Added:
The term “space” is also often used to refer to simplicial sets. In particular, Bousfield and Kan in their book “Homotopy Limits, Completions and Localizations” write:
“These notes are written simplicially, i.e. whenever we say space we mean simplicial set.
More recently, Jacob Lurie’s work continues this usage.
Added:
The term “space” is also often used to refer to simplicial sets. In particular, Bousfield and Kan in their book “Homotopy Limits, Completions and Localizations” write:
“These notes are written simplicially, i.e. whenever we say space we mean simplicial set.
More recently, Jacob Lurie’s work continues this usage.
1 to 28 of 28