Remove external dependencies from types/* (except Basics); close #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.
move decidable equality to Overture
Merge pull request #569 from mikeshulman/reorg2

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