Classic type theory textbooks

Although not as comprehensive a textbook as, say, Jech's classic book on set theory, Jean-Yves Girard's Proofs and Types is an excellent starting point for reading about type theory. It's freely available from translator Paul Taylor's website as a PDF. Girard does assume some knowledge of the lambda calculus; if you need to learn this too, I recommend Hindley and Seldin's Lambda-Calculus and Combinators: An Introduction.

As others have mentioned, Martin-Löf's Intuitionistic Type Theory would then be a good next step.

A different approach would be to read Benjamin Pierce's wonderful textbook, Types and Programming Languages. This is oriented towards the practical aspects of understanding types in the context of writing programming languages, rather than purely its mathematical characteristics or foundational promise, but nonetheless it's a very clear and well-written book, with numerous exercises.

The bibliography provided by the Stanford Encyclopedia of Philosophy entry on type theory is quite extensive, and might provide alternative avenues for your research.

There are two main settings in which I see type theory as a foundational system.

The first is intuitionistic type theory, particularly the system developed by Martin-Löf. The book Intuitionistic Type Theory (1980) seems to be floating around the internet.

The other setting is second-order (and higher-order) arithmetic. Two main books on this are Foundations without foundationalism by Stewart Shapiro (1991) and Subsystems of second order arithmetic by Stephen Simpson (1999). A decent amount of constructive mathematics, for example the material in Constructive Analysis by Bishop and Bridges (1985), can also be formalized directly in constructive higher-order arithmetic, however the taste of many constructivists is to avoid doing this.