Remove external dependencies from types/* (except Basics); close #567.

Closes #567.  This has three parts:

1. Prove directly in types/Equiv that Equiv is an hprop, and
derive there all the consequent theorems.  Now EquivalenceVarieties is
freed from having to do this, being instead just about comparing
definitions of equivalence.

2. Move everything from HProp that doesn't depend on types/* into
Basics/Trunc, and a few other things into types/Sigma.

3. Move Hedberg's theorem (used in types/Bool) from HSet into
Basics/Trunc.  This required using a different proof; the two in the
book depend on types/Paths and on EquivalenceVarieties.  I chose the
proof involving weakly constant functions.

I'm very open to criticism and suggestions.  I know at #567 @spitters was against having a separate file `types/Equiv`, and I'm not completely happy about it either; but it just didn't feel right putting all that stuff in `types/Universe`, and taken together it does in some ways have a similar feel to the other `types/` files.  If you still think, after looking at it, that it would be better in `types/Universe`, please do say so.  Note that I also made a `Types.v` file in the root, so that no one outside `types/` has to know about `types/Equiv`; they can just import `HoTT.Types`.
I think this (and `DecidablePaths`, if not the other classes too) belongs somewhere else in basics, perhaps Overture.    Or in their own file.  But I don't see any reason a priori why I should expect decidability to live in Trunc.