You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Alex Kreitzberg (Nov 19 2024 at 22:49):So, I've just started understanding Homotopy types from Baez's cohomology paper.
I'm pleasantly surprised that these seem to be the same types from Homotopy type theory.
I'm so pleased by this I wanted to try to make up a question about them.
Did Homotopy types get their name in anticipation of their application to type theory? Or is their name a coincidence?
I've always read "Homotopy type theory" as "homotopical style type theory" not as "the theory of Homotopy types." Where "Homotopy type" was a clearly understood topological space. I guess both reads are true, which is very fun!
Kevin Carlson (Nov 19 2024 at 22:52):Yes, I think it's a lucky post hoc pun; I think though I don't have a citation that the phrase "homotopy type" is 50-75 years old, much older than anybody would have been making the connection to type theory.
Alex Kreitzberg (Nov 19 2024 at 23:03):That makes me so happy, what a charming coincidence.
John Baez (Nov 19 2024 at 23:10):Did Homotopy types get their name in anticipation of their application to type theory?
No. Something called "the ramified theory of types" was invented by Bertrand Russell and Albert North Whitehead in their famous 1910-1912 book Principia Mathematica, which was trying to create a logical foundation for mathematics. To avoid paradoxes they built a rather elaborate theory of different "types" of set. I don't really understand it, so I'll quote a MathOverflow answer by Andreas Blass:
As far as I know, the word "ramified", in reference to type theory, means that one pays attention not only to the ranks of sets (where sets of rank n have members of rank n−1) but also to the complexity of their definitions. So for example, a set of fairly low rank, like a set of natural numbers, might be defined by a formula that quantifies over sets of high ranks and would be considered to have high "level". The comprehension axioms of such a type theory would impose limitations on both the ranks and the levels of the sets involved.
This rather complicated arrangement was introduced in Russell and Whitehead's "Principia Mathematica" to enforce predicativity of their type theory. Unfortunately, it proved too restrictive to serve as a foundation of ordinary mathematics, so it was supplemented with an "axiom of reducibility", saying that any set of high level is extensionally equal to (i.e., has the same members as) some set of suitably low level. Afterward (around 1920, I think) Chwistek and Ramsey (independently) noticed that the reducibility axiom had the effect of completely annihilating the structure of levels. So the theory can be reformulated by ignoring levels and working with ranks alone. This is now called either "simple type theory" or just "type theory".
The idea of levels resurfaced in Gödel's definition of the constructible universe .
Eventually this sort of type theory morphed into the quite different type theory used by logicians and later computer scientists - I have no idea how!
Quite separately, topologists like J. H. C. Whitehead - a completely different guy named Whitehead! - started talking about homotopy types . For example, in 1949 Mac Lane (yes, that guy) and Whitehead came out with a paper called On the 3-type of a complex. In this they classified what we'd now call homotopy 2-types (since they used a dumb numbering system). Even now people talk a lot about homotopy -types: we say two nice topological spaces have the same homotopy -type if they are homotopy equivalent up to dimension . I could be more precise, but this is the rough idea. And we say two nice spaces have the same homotopy type if they are homotopy equivalent.
It seems to be just a nice coincidence that these two things called "types" turned out to be related.
Alex Kreitzberg (Nov 19 2024 at 23:22):So, (J. H. C.) Whitehead studied (Homotopy) types :relieved:
Or just "Whitehead studied types" :face_with_hand_over_mouth:
There's a good joke hiding in there somewhere.
Mike Shulman (Nov 20 2024 at 00:17):Yes, the naming of the subject "homotopy type theory" was always a bit of a joke, or at least a double meaning: "homotopy (type theory) = (homotopy type) theory".
Mike Shulman (Nov 20 2024 at 00:17):Where "type theory" and "homotopy type" both had previous, unknown-to-be-related meanings.
Damiano Mazza (Nov 20 2024 at 08:21):Incidentally, it's funny to remark that this joke is not possible in Romance languages, so when translating "homotopy type theory" people have to choose whether "homotopy" refers to "type" or to "theory". Apparently, in Spanish it's "homotopy (type theory)" ("homotopy" becomes an adjective and the feminine singular inflection betrays it's related to the theory, not the types), while the French Wikipedia seems to suggest that, although "homotopy (type theory)" is more used, "(homotopy type) theory" is more correct (go figure why). This also makes me realize that I have always been translating it wrong: I would write "théorie des types homotopiques", which apparently isn't a thing (I never worked in homotopy type theory, I only had to write this in some French research projects and stuff like that, so it's ok :big_smile:). It also makes me wonder what people say in Italian, my native tongue... (the Italian Wikipedia doesn't have a page on homotopy type theory).
Damiano Mazza (Nov 20 2024 at 08:26):Anyway, +1 for English :wink:
Amar Hadzihasanovic (Nov 20 2024 at 09:12):I became curious about the invention of "homotopy type".
A quick search on Scholar seems to point to the 1935 book by Hopf and Alexandrov, "Topologie" (in German), as first introducing "Homotopietypus" to refer to the equivalence class of two continuous maps under the relation of homotopy.
In 1937, Borsuk (writing in French) then uses type d'homotopie, referencing Hopf and Alexandrov, in his paper Sur les transformations des polyèdres acycliques en surfaces sphériques, again only referring to the equivalence class of continuous maps under the homotopy relation.
Then in 1938 J.H.C. Whitehead speaks of the homotopy type of a simplicial complex in the modern sense, apparently for the first time in Simplicial spaces, nuclei and -groups. (As John points out, there is a shift in numbering so a 2-group for Whitehead seems to be the fundamental group). However Whitehead introduces the term quite casually in the introduction: the second paragraph starts with
Two complexes have the same m-group for each value of m if they have the same homotopy type.
which (at least to my "modern" ears) seems to imply an expectation that the reader will already know what this means.
Amar Hadzihasanovic (Nov 20 2024 at 09:13):The Hopf-Alexandrov book is the very first citation in Whitehead's paper as well, so it does seem to be the origin, but again, in the book the term seems to only ever be applied to maps and not objects.
Amar Hadzihasanovic (Nov 20 2024 at 09:17):It could be the case that the term had started being extended from maps to complexes in lectures/talks/private communication, so by the time of writing there was a common understanding and he didn't feel like it needed to be spelled out in the introduction.
(Later in the article Whitehead does give the explicit definition of "two complexes having the same homotopy type" as "there exists a homotopy equivalence between the two complexes", so it's not like it's entirely taken for granted).
Amar Hadzihasanovic (Nov 20 2024 at 09:36):Another interesting point is that in 1942, in On Rings of Operators. IV, Murray and von Neumann define the algebraical type and the spatial type of a ring of operators in a Hilbert space as being, respectively, its isomorphism class with respect to isomorphism of rings and with respect to isometric isomorphism.
These are first occurrences and the authors take a lot of care explaining the meaning of both terms, so it suggests that it is an early use of “type” to denote an equivalence class of objects under some notion of isomorphism. Could it have been influenced by the spread of "homotopy type"?
Amar Hadzihasanovic (Nov 20 2024 at 09:37):In 1940, Whitehead's On the homotopy type of manifolds was published in the Annals of mathematics, which is also where Murray and von Neumann published all the installments of On rings of operators, and presumably von Neumann would have been up-to-date with Annals-worthy developments.
Amar Hadzihasanovic (Nov 20 2024 at 09:46):Btw as a fun thing, I also came across a report of the 1st International Topological Conference in Moscow in 1935, whose list of attendees/talks sounds absolutely *insane*:
1.
James Waddell Alexander II (USA), “On the ring of a complex and the combinatory theory of integration.”2.
Pavel Sergeyevich Aleksandrov (USSR), “Some problems in set-theoretic topology.”3.
Garrett Birkhoff (USA), “Continuous groups and linear spaces.”4.
Nikolay Nikolayevich Bogolyubov and Nikolay Mitrofanovich Krylov (USSR), “Metric transitivity and invariant measure in dynamical systems of nonlinear mechanics.”5.
Karol Borsuk (Poland), “On spheroidal spaces.”6.
Nikolay Konstantinovich Brushlinskii (USSR), “On continuous mappings of spherical manifolds.”7.
Eduard Čech (Czechoslovakia), “Accessibility and homology.”8.
Eduard Čech (Czechoslovakia), “Betti groups with different coefficient groups.”9.
Stefan Cohn-Vossen (USSR), “Topological questions of differential geometry in the large.”10.
David van Dantzig (Netherlands), “Topological algebra.”11.
Vadim Arsenyevich Efremovich (USSR), “On topological types of affine mappings.”12.
Hans Freudenthal (Netherlands), “On topological approximations of spaces.”13.
Israel Isaakovich Gordon (USSR), “On the intersection invariants of a complex and its residual space.”14.
Poul Heegaard (Norway), “On the four-color problem.”15–16.
Heinz Hopf (Switzerland), “New research on n-dimensional manifolds.” Two talks.17.
Witold Hurewicz (Netherlands), “Homotopy and homology.”18.
Egbert Rudolf van Kampen (USA), “On the structure of a compact group.”19.
Andrey Nikolaevich Kolmogorov (USSR), “Homology rings in closed sets.”20.
Kazimierz Kuratowski (Poland), “On projective sets.”21.
Solomon Lefschetz (USA), “On locally connected sets.”22.
Andrey Andreyevich Markov, Jr. (USSR), “On the free equivalence of closed braids.”23.
Stefan Mazurkiewicz (Poland), “On the existence of indecomposable continua in sets of dimension
.”24.
Viktor Vladimirovich Nemytskii (USSR), “Unstable dynamical systems.”25.
John von Neumann (USA), “Integration theory in continuous groups.”26–27.
Jakob Nielsen (Denmark), Two talks on continuous surface mappings.28.
Georg August Nöbeling (Germany), “On the triangulability of varieties and main conjectures of combinatorial topology.”29.
Lev Semyonovich Pontryagin (USSR), “Topological properties of compact Lie groups.”30.
Georges de Rham (Switzerland), “On new Reidemeister topological invariants.”31.
Georges de Rham (Switzerland), “Topological aspects of the theory of multiple integrals.”32.
Julia Antonovna Różańska (USSR), “On continuous mappings of elements.”33.
Juliusz Schauder (Poland), “Some applications of the topology of functional spaces.”34.
Wacław Sierpiński (Poland), “On continuous mappings of sets.”35.
Wacław Sierpiński (Poland), “On transformations of sets by Baire functions.”36.
Wacław Sierpiński (Poland), “On a projective set of the second class.”37.
Paul Althaus Smith (USA), “Transformations of period two.”38.
Marshall Harvey Stone (USA), “Mapping theory in general topology.”39.
Albert William Tucker (USA), “On discrete spaces.”40.
Andrey Nikolayevich Tikhonov (USSR), “On invariant points of continuous mappings of bicompact spaces.”41.
André Weil (France), “Topological proof of Cartan’s theorem.”42.
André Weil (France), “Families of curves on the torus.”43.
Hassler Whitney (USA), “Topological properties of differentiable manifolds.”44.
Hassler Whitney (USA), “Sphere-spaces.”
John Baez (Nov 20 2024 at 15:14):If I went to that conference I'd have taken a big notebook and tried to collect signatures. I know and am awed by most of the speakers!
Mike Shulman (Nov 20 2024 at 15:58):I would definitely say that "homotopy (type theory)" is more correct. The other interpretation is more of a joke.
Mike Shulman (Nov 20 2024 at 15:59):Maybe anyone here who speaks a Romance language (or another language in which the pun doesn't work) can promulgate that.
Mike Shulman (Nov 20 2024 at 15:59):(Although I suppose it's possible that other homotopy type theorists might disagree with me.)
Mike Shulman (Nov 20 2024 at 16:10):Actually I'm confused. If "théorie des types d'homotopie" is "(homotopy type) theory", then the other option "théorie homotopique des types" mentioned on the French wikipedia sounds to me as though it should translate into English as "homotopy theory of types", which is different from "homotopy (type theory)".
Kenji Maillard (Nov 20 2024 at 16:23):I always only employed "théorie des types homotopique" in French, with the understanding that the whole type theory (théorie des types) is qualified by the homotopical qualificative.
Mike Shulman (Nov 20 2024 at 17:05):Is that phrase a pun in French like "homotopy type theory" in English then? Could you interpret it either as "(théorie des types) homotopique" or "théorie des (types homotopique)"?
Kenji Maillard (Nov 20 2024 at 17:30):No, the pun sadly does not work: I think the customary phrasing of homotopy types in French is "types d'homotopie" rather than "types homotopiques" (and then there's also a grammatical mismatch because "homotopique" is singular in the first case, but should be plural in the second).
Mike Shulman (Nov 20 2024 at 17:47):Ah, okay. So is "homotopy (type theory)" the only valid translation of "théorie des types homotopique"? Perhaps someone could edit the French wikipedia to at least include that as an option.
Damiano Mazza (Nov 20 2024 at 20:14):Kenji Maillard said:
I always only employed "théorie des types homotopique" in French
Ah, so I wasn't completely wrong! I just thought there was an "s" at the end, which is silent anyway so it sounds the same. But now I understand that "types homotopiques" simply doesn't exist, it's "types d'homotopie", as you say.
Damiano Mazza (Nov 20 2024 at 20:22):Mike Shulman said:
Ah, okay. So is "homotopy (type theory)" the only valid translation of "théorie des types homotopique"?
Yes. In fact, as Kenji says, "théorie des types homotopique" may be a better rendering of "homotopy (type theory)" than Wikipedia's "théorie homotopique des types", because it suggests that it's the whole "type theory" that is "homotopical", not just the "theory". But it's really a matter of taste, technically the adjective "homotopique" is related to the noun "théorie", whether you place it right after or at the end, so both expressions literally translate in English as "homotopical theory of types" (admitting that the adjective "homotopical" exists in English, which I am not sure it does). The literal translation of the other option mentioned on Wikipedia is "theory of types of homotopy".
Damiano Mazza (Nov 20 2024 at 20:25):I will leave editing Wikipedia to someone more authoritative than me on the subject (both linguistically and scientifically)...
Mike Shulman (Nov 20 2024 at 21:14):Interesting, thanks. I feel authoritative scientifically to edit Wikipedia, but not linguistically.
Mike Shulman (Nov 20 2024 at 21:14):The adjective "homotopical" does certainly exist in (mathematical) English, e.g. [[homotopical category]].
Damiano Mazza (Nov 20 2024 at 22:08):Actually, now that I think about it, I don't understand why people, both in Spanish and French, resorted to the adjective "homotopical" to render "homotopy (type theory)".
English compound nouns of the form "X Y" where both X and Y are nouns are rendered in Romance languages as "Y of X". E.g. "work permit" becomes "permit of work". Similarly, "type theory" = "theory of types", "homotopy type" = "type of homotopy", and also "homotopy theory" = "theory of homotopy".
Following the above, "(homotopy type) theory" becomes "theory of types of homotopy", which, as I mentioned, is the literal translation of "théorie des types d'homotopie". But then "homotopy (type theory)" should become "theory of homotopy of types", which is the literal translation of "théorie de l'homotopie des types". As far as I know, nobody has ever used this expression in French, but to me it sounds like a very adequate description of the subject, possibly more than both expressions using the adjective "homotopique"/"homotopical". I mean, isn't HoTT about seeing types as spaces, and then studying them from the viewpoint of homotopy theory?
Of course I am not advocating for changing the terminology, it's just curious that the most direct and obvious translation isn't the one that ended up being used.
Mike Shulman (Nov 20 2024 at 22:11):Some people in English have said "homotopical type theory", particularly I think in the early days of the subject before terminology settled down. Maybe the Romance languages picked up on that and then didn't settle the same way English did.
Damiano Mazza (Nov 20 2024 at 22:11):Ah, that makes sense!
Amar Hadzihasanovic (Nov 21 2024 at 06:12):To me "théorie de l'homotopie des types" seems more appropriately translated as "homotopy theory of types", which I think has a quite different nuance than "homotopy (type theory)"...
Vincent R.B. Blazy (Nov 21 2024 at 12:44):Amar Hadzihasanovic said:
Another interesting point is that in 1942, in On Rings of Operators. IV, Murray and von Neumann define the algebraical type and the spatial type of a ring of operators in a Hilbert space as being, respectively, its isomorphism class with respect to isomorphism of rings and with respect to isometric isomorphism.
These are first occurrences and the authors take a lot of care explaining the meaning of both terms, so it suggests that it is an early use of “type” to denote an equivalence class of objects under some notion of isomorphism. Could it have been influenced by the spread of "homotopy type"?
Yes, didn’t know those ones but there are order types, too! I don’t know since when and whom, that said…
Amar Hadzihasanovic (Nov 21 2024 at 13:59):Good point @Vincent R.B. Blazy . Order type had a much older history: it seems to date back to a 1884 paper by Georg Cantor, Prinzipien einer Theorie der Ordnungstypen.
Amar Hadzihasanovic (Nov 21 2024 at 14:04):So it seems plausible that in the 1930s mathematicians start thinking more and more about "notions of isomorphism" and equivalence classes under those notions, and they have "order types" as the obvious already-established instance that can be generalised.
Amar Hadzihasanovic (Nov 21 2024 at 14:18):Obviously Russell was deeply influenced by Cantor, so it would be very neat if somehow also his use of "type" had its origin in Cantor, but that seems a bit of a stretch :)