HoTT/book — pull request #584 by Shark64 (2013-12-13 20:25:42+00:00)
Title: enable pdftex extensions with \usepackage{microtype}

I've tried to enable microtype and seems to work well (fewer overfull hboxes).
The only problem was hyphenation of 2 section titles, but disabling tracking on those 2 pages seems to fix it.