More notation fixes

The main reason for this pull request is to put `'o'` inside of a scope; when trying to port my category theory library to be built on top of HoTT, I discovered that I couldn't effectively use `'o'` as a notation after importing HoTT because it got stuck in the default scope.  I figured I'd also put the other notations in scopes while I was at it; it's much easier to overwrite a notation or hide it, should you want to, if it's in a scope.

I've checked to make sure that the library still compiles.  One backwards-incompatible change is that we'll now need to `Open trunc_scope` to use the `<=` notation for truncation.  This can be remedied by opening it globally in `Overture.v`, if that's desirable.

If you want, I can remove the churn caused by emacs removing trailing spaces, but I figured I'd leave it in unless told otherwise.