In homotopy type theory, homotopy types can be viewed as logical types and it is possible to prove some theorems about them without using any underlying space (no simplicial set, no topological space). It is a kind of synthetic algebraic topology. Is it just a coincidence that the word "type" may have these two meanings ? What I mean is: what had in mind the one who invented this terminology of "homotopy types" ? And do we even know where that terminology of "homotopy types" comes from. I guess that the answer will be that it is a coincidence but since it is written nowhere in the book, I ask the question in order to be sure.
$\begingroup$
$\endgroup$
8
-
7$\begingroup$ Il faut demander au type qui a inventé le terme. $\endgroup$– Jonathan ChicheCommented Aug 6, 2013 at 14:54
-
13$\begingroup$ It's a coincidence, but a very fortunate one (for a change). When people started saying "homotopy type" X they meant "the type of X" as in "what kind of space is X". When people said "type" X in logic, they meant the type of its terms, as in "what kind of thing is an $x \in X$ ". In a naive sense, these two usages of "type" are not actually the same. Luckily, as one digs deeper, it turns out by lucky coincidence that at the bottom of it indeed this is the same notion of "type" in both cases. I think its one of those trivialities that deserve to be regarded as "deep". $\endgroup$– Urs SchreiberCommented Aug 6, 2013 at 14:59
-
3$\begingroup$ @Jonathan Chiche: oui en somme, il nous faut faire la rencontre du troisième type. $\endgroup$– Philippe GaucherCommented Aug 6, 2013 at 19:11
-
4$\begingroup$ It seems that HoTT is fashionable enough that the hawks have not descended on this question and branded it as "soft" and "not mathematical". $\endgroup$– Andrej BauerCommented Aug 6, 2013 at 19:19
-
$\begingroup$ I am inclined to think that this is not a mere coincidence. Rather, that this is some sort of reflection of the fact that mathematicians tend to think in predicable ways. $\endgroup$– Baby DragonCommented Aug 6, 2013 at 19:21
|
Show 3 more comments
2 Answers
$\begingroup$
$\endgroup$
1
Maybe I should repost my comment above as a genuine answer:
It's a coincidence, but a very fortunate one (for a change).
When people started saying "homotopy type" $X$ they meant "the type of $X$" as in "what kind of space is X?".
When people said "type" $X$ in logic (type theory), they meant the type of its terms, as in "what kind of thing is an $x \in X$?".
In a naive sense, these two usages of "type" are not actually the same. Remarkably, as one digs deeper and understands that intensional type theory is essentially homtopy type theory, it turns out by lucky coincidence that at the bottom of it indeed this is the same notion of "type" in both cases.
I think its one of those trivialities that deserve to be regarded as "deep".
answered Aug 6, 2013 at 20:53
-
$\begingroup$ The motivation of this question was the reading of chapter 8 of the book. It is the first (soft and non-mathematical) question which came to mind. $\endgroup$ Commented Aug 7, 2013 at 2:25
$\begingroup$
$\endgroup$
There seem to be at least two distinct traditions in mathematics for the use of 'type'.
The 'Homotopy types' of algebraic topology seem to have been defined in analogy to 'order types'. Two ordered sets have the same order type when they are isomorphic. Cantor defined the ordinal numbers to be the order types of well-ordered sets. I have not checked whether he used the German equivalent of the word 'type'.
The 'intensional types' of HoTT originate with Bertrand Russell's approach to resolving his paradox by requiring each mathematical object to be of some type, with constraints on which objects are allowed to belong to any given type. Any formal quantifier could only be a quantifier over some type. This was in contrast to Frege who allowed all of his objects to belong to a single realm which could be quantified over.
No doubt both traditions have a source in everyday usage; e.g. from the free dictionary
Type: A number of people or things having in common traits or characteristics that distinguish them as a group or class.
