HoTT/HoTT — pull request #160 by JasonGross (2013-08-01 16:56:20+00:00)
Title: Fix a typo, FunExt -> Funext; now things compile

I believe this was due to a merge conflict between
74fddcd8b492cfa92874d606c6e3d6b9629a28ad and
64dcc4f24a23ff532ff27f2e44980e9faf39e0da. I think this was because
e4f905e4afbc55f6f0bc0011f00bd3c5885a2849 was a merge from HoTT/HoTT,
rather than a rebase on top of it.