[ek]

It seems like I end up plugging the book really frequently here, but it's for good reason -- it's exceptionally readable AND it's accompanied by a full Coq development. That is, you can do basically every exercise in the book, directly in Coq, if you want.

You can definitely just read the material and then come back and try the exercises in Coq later, or more tightly couple the two. I think either approach would work well, and it's up to personal preference.

The first chapter of HoTT is an introduction to Martin-Löf that I personally find quite intuitive, to the point that I'd say it's clear than most other expositions of the same material that I've tried to read.

It will be easier to understand dependent type theory if you're programmed in a dependently typed language, but I wouldn't say it's strictly necessary to understand dependent types theoretically. I have just a little bit of Coq experience and found myself comfortable with the HoTT presentation of dependent types.

[tel]

I have only managed to get through the first chapter myself and I really want to reiterate that—the first chapter does a fantastic job presenting MLTT.

[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.