[codeismath]

I found the first 6 chapters of "Type Theory and Formal Proof" to be amazing for covering the beginning math behind Type Theory. The authors (Nederpelt and Geuvers) don't gloss over assumptions and they build things up step by step. I didn't study this in university but have picked up many books along the way. I'm usually quite lost within the first 10 or 20 pages until picking up Type Theory and Formal Proof. This one took me somewhere between 100 to 200 pages before getting lost. They cover the entire lambda cube.

But then I was able to re-start Thompson's "Type Theory and Functional Programming" and it was clear that I started to understand a lot of it.

If you enjoy the nostalgia of older books like me, then pick up an original copy of "Intuitionistic Type Theory" edited by Per Martin-Löf.