[yetanotherphd]

thanks for the pointers. I gave up with Martin-Löf type theory reading other texts, so I'm looking forward to trying again with this book.