About the state of art that I'm running ahead of Type Theory I have the these questions all related about history of Types.
- Where did the idea of Type come from? (It seems that all start when Russell and Whitehead propose a way to avoid the contradiction that we know today as Russell's Paradox, am I right?)
- Before considering the type concept, was there something similar? (Maybe a refinement of a set, but I don't find a reference distinct of Russell).
- Who was the first person to put it on formal terms? (Was Russell with this paper of 1908 or ?