Type theory is a rapidly developing topic at the intersection of logic, computer science, and mathematics. Graduate students and researchers who need to comprehend the inner workings of the mathematical machinery, the function of logical principles within, the crucial contribution of definitions, and the critical nature of well-structured proofs will benefit greatly from this gentle step-by-step introduction. Beginning with untyped lambda calculus, the authors move on to a number of fundamental type systems, including the well-known and potent Calculus of Constructions. The fundamentals of proof building and checking are also covered in the book, along with dependent type theory’s application to the formalization of mathematics. The sole need is a fundamental understanding of undergraduate mathematics. The entire idea is shown with carefully picked instances. Each chapter concludes with a summary of the key points, some background information, reading recommendations, and a number of exercises to assist readers to become more familiar with the subject matter.