Fix a typo, FunExt -> Funext; now things compile

I believe this was due to a merge conflict between
74fddcd8b492cfa92874d606c6e3d6b9629a28ad and
64dcc4f24a23ff532ff27f2e44980e9faf39e0da.  I think this was because
e4f905e4afbc55f6f0bc0011f00bd3c5885a2849 was a merge from HoTT/HoTT,
rather than a rebase on top of it.
Fix library so that it works with the newest coq

Closes #152
Make Unit a Set

Having Unit in Prop causing issues and universe inconsistencies, such as
https://github.com/HoTT/coq/issues/50.
Add priorities to typeclass instances

The default priorities are rediculously high (small numbers), equal to
the number of (typeclass?) arguments to the instance.  Instead, I've
defaulted to 1000 for most instances, 10000 for the instances that are
likely to lead to cycles or information flow in the wrong direction, 100
for instances which I think are likely to lead to speedy resolution, and
0 for instances which have no typeclass arguments (and thus discharge
their goals immediately).  (Smaller numbers are higher priority.)

Additionally, I have renamed [Contr] to [Contr_internal] and made
[Contr] a notation for [IsTrunc minus_two].  This, combined with the
fact that [IsTrunc] is now [Opaque] in typeclass search, breaks [Contr]
-> [IsTrunc] -> [Contr] cycles.  We now only do typeclass search on
[IsTrunc].  This requires iota-expanding a few instance declarations of
[Contr], to get around deficiencies in Coq's typeclass machinery; I've
submitted a bug report at
https://coq.inria.fr/bugs/show_bug.cgi?id=3101.

Now that all the instances are global, we pick up some instances in
FunextVarieties.v; I've removed the confused comments and explicit
instances.

I remove [hprop_forall] and the associated comment, because we have
[trunc_forall].

I've added some [Hint]s to typeclass search which trigger early and set
up the goal.  It seems to me that we generally want to reason about
[IsTrunc (S n) A] rather than [IsTrunc n (a = b)]; the opaqueness of
[IsTrunc] (only to typeclass resolution), [istrunc_paths], and the [Hint
Extern]s I've added to [Overture.v], implement this.

The instance [contr_trunc_minus_two] is no longer; it's not useful,
because we instead want to use [progress change].  If we don't then we
can get into infinite loops because [contr_trunc_minus_two] can, up to
unificiation, be applied an arbitrary number of times.

There are a few proofs where I've changed [auto] to [auto with
typeclass_instances]; [auto] doesn't always work any more, though I
haven't looked into it very closely.  I think it's reasonable to need to
inform Coq that you're doing typeclass resolution.

The proof of [trunc_equiv] needed to be modified so we don't loop
infinitely on [eapply I].  I'm annoyed that the context seems to take
precedence over cost 0 hints.  However, this is a fairly foundational
proof, and I don't anticipate this kind of problem popping up in
typeclass search often.

This makes my category theory library compile twice as fast, and doesn't
significantly effect the total compile time of the HoTT library.
Merge pull request #163 from JasonGross/category-theory-prs

Combine a few pull requests needed for my category theory library