Homotopy Type Theory (Univalent Foundations for Mathematics)

A dry topic - but the authors manage to convey their enthusiasm and make a lot of effort to pick up the uninitiated

Lots of background and historical references