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.
Remove use of FunextAxiom and UnivalenceAxiom
Move some per-lemma variables to section contexts

I'm not sure which is the preferred style, but Bas told me that there
was some kind of problem in ObjectClassifier with not assuming
Univalence or Funext as an axiom.  I tried to track it down, but
everything seems to work fine.
Merge pull request #140 from JasonGross/axiom-removal

Axiom removal
Define [f_ap] to replace the late [f_equal]

I'm not sure exactly how [f_ap] differs from [f_equal], as I've not
looked at the ml definition of [f_equal].  I've included a fairly
lengthy comment explaining how [f_ap] works, and included a note about
generalizing it.

This closes #139.
Make the issig tactics give better error messages
Fix a name error

Oops.  I neglected to check that a last-minute change I made to
8add452dbeb0b517a36708c07e11a2166ed2d952 worked.
Merge pull request #141 from JasonGross/f_equal

Define [f_ap] to replace the late [f_equal]
Adding Section, explicit name to avoid
  Error: H is already used.
Merge branch 'master' of https://github.com/HoTT/HoTT
Merge pull request #144 from JasonGross/issig-error-messages

Make the issig tactics give better error messages
Merge pull request #143 from JasonGross/fix-names

Fix a name error
Update Forall.v

Variation on dpath_forall
Fiddling.

Signed-off-by: jcmckeown <jesse@sockwright>
Use polymorphic [Axiom]s, not the [admit] exploit

The newer versions of HoTT/coq support polymorphic axioms, and no longer
require the [admit] exploit.  This way, we have two fewer top-level
constants floating around.