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.
Prefix [Instance] with [Global]

[Instance]s are, by default, local to sections.  I've gone through and
prefixed all of the [Instance]s inside [Section]s of with [Global], so
they get picked up by typeclass search.  I don't think I missed any, but
I'm not sure.

This is especially useful for developments building on top of this
library which simply [Import HoTT] and want to prove contractibility
facts in an automated fashion.
Stick [Context `{Funext}.] inside a section

[Context] is only meant to be used for local assumptions, not axioms.
And this files doesn't import the funext axiom file, so I assume this is
meant to be local.
Remove an [Existing Instance]

We don't need it, now that we declared that using [Global Instance]
rather than just [Instance] in a section.
Merge pull request #133 from JasonGross/more-notation-fixes

More notation fixes
Merge branch 'instances' of https://github.com/JasonGross/HoTT

Conflicts:
	theories/hit/minus1Trunc.v
Merge branch 'funext-not-axiom' of https://github.com/JasonGross/HoTT into JasonGross-funext-not-axiom

Conflicts:
	theories/hit/minus1Trunc.v