Yes.  But I felt that I had nit-picked enough at this pull request, and this moves the pre-existing notations, rather than adding them, so I'm fine with removing them separately in another pull request and not making @spitters change more things.  Alternatively, @spitters, you can include that commit here with `git remote add JasonGross https://github.com/JasonGross/HoTT.git; git remote update; git cherry-pick b7b76f33adabf469c6c9dc14d3e2aa7e1af5cdf4` and then pushing to the pull request.