I love this. It looks like this covers a very practical version of a similar buildup that I like [0]. The book I linked is a much shorter textbook path through these type systems than the books linked in the article, and I found it pretty readable.
[0] https://anggtwu.net/tmp/nederpelt_geuvers__type_theory_and_f...
While that is an excellent book, I would say that it focuses on type theory from a somewhat more theoretical perspective than (say) TAPL which is more on type _systems_ from a programming languages perspective. Both are great reads though.