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 sayspacewe meansimplicial 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 sayspacewe meansimplicial set.

More recently, Jacob Lurie’s work continues this usage.

]]>This entry was (and is) lacking references. I have now, at least, added pointer to:

- Jacob Lurie, Section 1.1.2 in:
*Higher Topos Theory*, Annals of Mathematics Studies 170, Princeton University Press 2009 (pup:8957, pdf)

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 $d \circ d = 0$. 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.

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

]]>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 #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 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?

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

]]>Re #18: One truly depressing aspect is that we still don’t know how to define (∞,1)-categories in homotopy type theory.

]]>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?)

]]>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?)

]]>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”?

]]>Explicitly saying that “anima” is a synonym for infinity groupoid, since this wasn’t explicit in what was there before. I hope this is right! Googling “anima” and “condensed anima” yields pages on psychology and World of Warcraft respectively…

]]>Trying to fix up the “Relation to infty-groups”-section.

]]>Those are just the 0-truncated ones. (-:

]]>Re #11: Doesn’t “type” also refer to types in extensional type theory, which are not at all like homotopy types?

]]>Only “space” can compete with it

What about “type”?

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

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

]]>“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.

]]>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, …).

]]>I have to say that I am not animated by the terminology “anima”.

]]>Move terminology section to the end, since some of it is fairly idiosyncratic and shouldn’t be emphasized to a newcomer. Also move the more common usages to the top of the section and add historical comments.

]]>