We do not need this.  See https://github.com/JasonGross/HoTT/commit/36a9ab2.  You can add this commit to your pull request by running `git remote add JasonGross https://github.com/JasonGross/HoTT.git && git remote update && git cherry-pick 36a9ab2` (and then pushing to github).