A beautiful book, written in the "The Little..." series' question and answer format. A challenging topic but just about as accessible as I can think anyone can make it. Warmly recommended if you want to know what dependent types are all about.