HoTT is really fun. I'm particularly interested to see if the computational behavior of univalent and higher inductive types gets sussed out (or else, like Bob Harper, I shall have to pick up my toys and head home). Computing with univalence and HITs sounds lovely, if only we could figure out how to do it...
What is a good way to get started with this literature? And is it better to read theory first, or read theory in conjunction with using languages like Haskell and Coq?
I studied a lot of mathematics, and I find this fascinating, but I've found it hard to read the literature on type theory, and mathematical logic also.
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.
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.
