HoTT/book — pull request #474 by andrejbauer (2013-09-19 11:43:15+00:00)
Title: Remove duplicate words

I ran a regular expression to find all duplicate words (such as "the the") and fixed them (manually confirming the fixes).