Add coq-HoTT as a dependency for the .vo files

Some basic testing suggests that this will cause `make` to auto-re-coq
the .v files whenever you `git submodule update`, i.e., when it's
possible to tell that the version of Coq we're using has changed.
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 github.com:HoTT/HoTT
trivial changes from @spitters
Merge pull request #495 from mikeshulman/master

trivial changes from @spitters
Merge pull request #487 from spitters/master

General Subobjectclassifier
Merge branch 'master' of github.com:HoTT/HoTT
make Trunc not depend on types/*
move basic files to Basics/*
fix pointer to Overture in configure.ac
remove no-longer-necessary Scheme hackery in Overture
appcontext is deprecated, use context instead; close #497
Merge pull request #499 from mikeshulman/appcontext

appcontext is deprecated, use context instead; close #497