If your interest is type theoretic foundations, you might want to look into modern (type-theory based) theorem provers. This is how I learned both type theory and dependent type theory. This has the following advantages:
- Proof assistants let you "program in type theory". This ability to manipulate type theoretic objects (and have a compiler yell at you when you do something wrong) was really helpful for me.
- Like Principia Mathematica, modern theorem provers are designed to be foundations of mathematics that can be used to formally prove theorems in mathematics. And unlike ZFC (or even Principia), these systems are practically useable. (Now, "practical" is relative. They still are too cumbersome for a typical working mathematician, but they have nonetheless been used to formally prove a number of major theorems in mathematics.)
- The tutorials for these theorem provers are well-written, designed for a broad audience, and are not quite as intense as say the Homotopy Type Theory book.
There are some disadvantages to this approach.
- The tutorials I am about to list don't give much, if any, meta-theory on type theory. While they will teach you how to prove things in type theory, they don't give proofs about type theory.
- Another disadvantage is that they might be a bit more geared to those who are CS literate.
I am biased since one of the authors is my advisor, but Theorem proving in Lean is a great way to learn dependent type theory and the Lean proof assistant. It even has an online environment to try things out without having to install any software.
It is much older, but I also found the HOL-Light tutorial to be a good way to learn a weaker type-theoretic proof system.