Put 'o' in a scope.

This way, it can be used in libraries building on top of HoTT for, e.g.,
morphism composition and functor composition and function composition
all at once.

Ideally, Coq would have a special [function_scope] like [type_scope].
I've opened https://coq.inria.fr/bugs/show_bug.cgi?id=3080 for this.  In
the meantime, we just have to open whatever scope we put it in,
globally.
Change the level of the infix == notation

This way it's more compatible with the standard library, e.g.,
theories/Classes/SetoidClass.v.

Also, put it in [type_scope], because it's only useful when Coq is
expecting something of type [Type], and because scoped notations are
nicer to deal with when building on top of libraries.  We might instead
want to put it in its own scope, like how there is a different variant
in [Q_scope] in the standard library, but [type_scope] is a reasonable
default.
Move the truncation notations inside a scope.

Again scoped notations are nicer for building on top of.  This change
will require us to [Open Scope trunc_scope] whenever we want to use the
[<=] notation for truncation levels, unless we open it globally in
Overture.
Merge pull request #133 from JasonGross/more-notation-fixes

More notation fixes