HoTT/HoTT — pull request #426 by JasonGross (2014-08-07 16:46:28+00:00)
Title: Add a .mailmap file

This will make the [github contributors page](https://github.com/HoTT/HoTT/graphs/contributors) display more people and more accurate numbers. I'm going to push this directly, as it doesn't touch any HoTT stuff, but feel free to update it so that it picks your preferred email address, or your preferred name formatting, etc.