Yes, Homotopy Type Theory is the latest, greatest, thing (we are told). Yes, a free book is available, following on from a major year-long program at the Institute for Advanced Study at Princeton in 2013-13, and this will tell you lots about the current state of play. And yes, you too started the book and found it pretty impenetrable. What on earth is going on?

Help is at hand.

Robert Harper at CMU ran a grad course last semester, ‘Introducing Homotopy Type Theory’. Notes written up by his students are online. So too are videos of his lectures (use the “stay on the web” option if visiting the site on an iPad). This all looks a pretty good way in if you are still curious about the HoTT phenomenon.