From the Introduction section of Homotopy Type Theory book:
Type theory was originally invented by Bertrand Russell ... It was later developed as a rigorous formal system in its own right(under tha name "$\lambda$-calculus").
Can anyone explain me this sentence? I'm having trouble seeing $\lambda$-calculus as a type system.
(also in the same paragraph, $\lambda$-calculus called as "Church's type system")