The term type actually originates way before that, the 19th century meaning is "category with common characteristics", which is how we use the word in normal discourse (Python is a type of programming language....).
Bob Harper has adopted a very narrow definition of type based on one discipline, type theory, but the word "type" itself is much more general than that. I definitely use the word "type" when talking about my Python programs, even if there are no static type theoretic types to be seen.
In a dynamically typed language, your proofs are checked at run-time, which has everything to do with types! Getting a type error at run-time is much better than having the program keep going and produce a wrong result (if it doesn't core dump via memory corruption first).
Dynamic dispatch doesn't even play into it.
