Fix frudenthal, reorder Truncation_functor args

Now, when you [apply Truncation_functor], you're not left with a goal of
[Univalence].  However, this isn't a satisfactory solution; perhaps
@mikeshulman can help solve the remaining goal involving
[truncation_incl] and [Truncation_functor] which used to go through
judgmentally?
Merge pull request #492 from JasonGross/fix-freudenthal

Fix frudenthal, reorder Truncation_functor args
Add toploop to coq, so hoqtop -help succeeds
include predicate as redundant data in UnitSubuniverse
include induction principle as redundant data in Modality
make that bit of Freudenthal work
remove "using n" to make the proofs work.
revert some Univalences to Funexts
remove nearly all univalence in ReflectiveSubuniverse and Modality
Merge pull request #493 from mikeshulman/modalitydata

Include useful redundant data in modalities
Merge branch 'master' of https://github.com/HoTT/HoTT
names updated to Book_X_Y_zzzz