What is your goal? Type theory is at the intersection of programming languages and logic. If you care about programming languages and type systems, read TAPL:
If you care about type theory purely as a logic, I don’t have an obvious recommendation, but could point you at some material.
(Programming Languages researcher)
The goal is mainly to understand its relation to proof assistants, I have experience with it before as a purely logical study but i haven’t tried to see it in this new context for myself. This book looks excellent though, thank you for your recommendation
Ah, then you’ll want to read about the [https://hal.inria.fr/inria-00076024/document](Calculus of Constructions):
Yeah, TAPL is the book on type systems. I’m not aware of competition.
Seconding TAPL, it was the textbook for the type theory course I took in college, it is topnotch.