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 $P : \Delta^\mathrm{op} \to \mathrm{Type}$ such that $P(\Delta^n)$ is the type of $n$-long strings of composable arrows. Then the (∞,1)-categories would be the one where the degeneracy $P(\Delta^0) \to P(\Delta^1)$ 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 $X\colon\Delta^op \to Type$, and it is not at all clear how to encode all coherences here: for each $[n]\in\Delta^op$ we have a type $X_n$, for each $a\colon[m]\to[n]$ we have a map $X_a\colon X_n\to X_m$, for each $a\colon[l]\to[m]$ and $b\colon[m]\to[n]$ we have $X_{a,b}:X_b\circ X_a = X_{b\circ a}$, 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.
1 to 23 of 23