I learnt it from "Type Theory and Formal Proof" when I wanted to understand type theory (I was in a community of functional programmers). BTW, nice book, I alwa

I learnt it from "Type Theory and Formal Proof" when I wanted to understand type theory (I was in a community of functional programmers). BTW, nice book, I always recommend it to absolute beginners.