Type Theory for Beginners

One of the first things one learns at university are some foundations of mathematics. This covers topics such as sets, functions between sets, relations, logic & proof, ...

I learned this stuff too. But it does not satisfy me because some things seem to be too unnatural for me. In this blog post, Dr. Shulman explains that these problems with the "standard" foundations (ZFC, ETCS) are solved by type theory.

The standard reference to learn type theory is the Homotopy Type Theory book. But this book is too complicated for me, since I am a beginner. That is why I am searching for material from which I can learn type theory. This material should be written for the same audience for which the introductions to sets, functions, ... mentioned above are written.

I don't have the perfect book reference for you, but here are some references that I think are worth looking at with your background. At least you could give them a try.

(1) The HoTT lectures by Robert Harper

There is a course held by Robert Harper available here. It is not easier to understand but it contains a lot of tiny hints and explanations which may help you understand parts of book. There are excellent videos, notes and exercises included.

Do not be demotivated if you don't understand everything. But again: The hints you get there pay off when you continue reading material about type theory.

(2) The book "Types and Programming Languages" by Benjamin Pierce

It describes many aspects of Type Theory from a (as the title implies) more programming language oriented perspective while covering a lot basic material, which may is exactly what you're looking for.

(3) Start learning a statically typed programming language

To turn this into a a book reference: There is a book called "Software Foundations" by Benjamin Pierce, too. It covers a very good beginner-friendly introduction to Coq, a programming language widely used in the type theory ecosystem. Bonus: It introduces type theoretic concepts on the fly including immediate applications implemented in Coq.

You could also try Agda, Haskell or Idris, too. In fact using a programming language like the one mentioned is in some sense "applying" type theory. They provide a good learning environment and most probably this will generate a lot of insights in type theory for you when combined with other learning resources.

Last year I put together a page for exactly this purpose, outlining what I would consider the optimal path through learning Type Theory

http://purelytheoretical.com/sywtltt.html