Why was there a need for Martin-Löf to create intuitionistic type theory? I've been reading up on Intuitionistic Type Theory (ITT) and it does make sense. But what I'm struggling to understand is "why" was it created in the first place?

Intuitionistic Logic (IL) and Simply-typed $\lambda$-calculus (STLC) and type theory in general predates the very existence of Martin-Löf himself! It seems that one can do everything in STLC that is doable in ITT (I may be wrong, but at least it feels that way).  

So what was "novel" about ITT and how exactly did (or does) it advance the theory of computation? From what I understand, he introduced the notion of "dependent types", but it seems they were already there in STLC, in a way. Was his ITT an attempt at abstraction to understand the underlying principles of STLC and IL together? But didn't STLC already held do that? So, just why was ITT created in the first place? What is/was the point?

Here's an excerpt from Wikipedia: But I still don't get the reason behind its creation that didn't already exist before.


  Martin-Löf's first draft article on type theory dates back to 1971.
  This impredicative theory generalized Girard's System F. However, this
  system turned out to be inconsistent due to Girard's paradox which was
  discovered by Girard when studying System U, an inconsistent extension
  of System F. This experience led Per Martin-Löf to develop the
  philosophical foundations of type theory, his meaning explanation, a
  form of proof-theoretic semantics, which justifies predicative type
  theory as presented in his 1984 Bibliopolis book...


It seems from the excerpt that the reason was to develop the "philosophical foundations of type theory" - I thought this foundation already existed (or maybe I assumed it did). Was this the main reason then?
Very briefly: the simply-typed $\lambda$-calculus does not have  dependent types. Dependent types were proposed by de Bruijn and Howard who wanted to extend the Curry-Howard correspondence from propositional to first-order logic. The key contribution of Martin-L&ouml;f's is a novel analysis of equality.
There are two main ways of giving Curry-Howard style account of equality. 


Using Leibniz's rule of the identity of indiscernibles to encode propositional equality . This approach is used in the calculus of constructions, but it requires impredicative universes which were rejected by Martin-L&ouml;f for philosophical reasons.
A direct constructive characterisation of equality. Giving such a characterisation using identity types might be the main novelty of Martin-Löf's intuitionistic type theory.


Identity types appear deceptively simple today, but they refocussed the understanding of type-theory partly because they gave rise to intriguing semantical questions such as: are identity proofs unique? In some sense this question lead to homotopy type theory and the univalence axiom (which is incompatible with the uniqueness of identities). That the uniqueness of identity proofs is not derivable in Martin-Löf's intuitionistic type theory was shown 
by Hofmann and Streicher in: "The groupoid interpretation of type theory". Incidentally, this result also shows that pattern matching is not a conservative extension of traditional type theory.