# A (very naive) question about Homotopy Type Theory

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.

-
Il faut demander au type qui a inventé le terme. –  Jonathan Chiche Aug 6 '13 at 14:54
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". –  Urs Schreiber Aug 6 '13 at 14:59
@Jonathan Chiche: oui en somme, il nous faut faire la rencontre du troisième type. –  Philippe Gaucher Aug 6 '13 at 19:11
It seems that HoTT is fashionable enough that the hawks have not descended on this question and branded it as "soft" and "not mathematical". –  Andrej Bauer Aug 6 '13 at 19:19
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. –  Baby Dragon Aug 6 '13 at 19:21

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

-
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. –  Philippe Gaucher Aug 7 '13 at 2:25