Update STYLE, incorporating wiki; close #468
improvements to STYLE based on comments
further additions, remark on :>
improvements to STYLE from suggestions
fix typo in STYLE
use GFM with highlighting for Coq code blocks
make hSet and hProp special cases of TruncType
Merge pull request #559 from mikeshulman/style

Update STYLE, incorporating wiki; close #468
Move TruncType to Basics/Trunc
remove workaround for fixed bug 117
Merge pull request #566 from mikeshulman/trunctype

make hSet and hProp special cases of TruncType
Merge pull request #568 from mikeshulman/bug117

remove workaround for fixed bug 117
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
rename types/ to Types/
Merge pull request #569 from mikeshulman/reorg2

Remove external dependencies from types/* (except Basics); close #567.
Merge pull request #572 from mikeshulman/renametypes

Rename types/ to Types/
color Types rather than types
Merge pull request #574 from mikeshulman/master

color Types rather than types
more color fixes