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