Question for the author: what books do you recommend for a gentle but still substantive introduction to type theory? Books such as Pierce get super complex very fast. Thanks!