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...