Make travis test for axiom dependence

Now travis will enforce the convention that nothing in the library
should depend on FunextAxiom or UnivalenceAxiom.
Add some instances about truncation of IsTrunc
Merge pull request #398 from JasonGross/istrunc-instances

Add some instances about truncation of IsTrunc
Merge pull request #397 from JasonGross/check-no-axiom

Make travis test for axiom dependence
Less restrictive Funext_downward_closed

Funext has three universes, and we want them all to be independent; this
seems to be necessary to eliminate universe inconsistencies in the
latest version of trunk.
Fixups to work with the latest polyproj branch.
Progress on adapting HoTT and categories to latest polyproj branch.
Progress on adapting HoTT and categories to latest polyproj branch.
Adapt categories and hit's code to latest polyproj (Private keyword).
- A few places raise universe inconsistencies in Categories still, not sure why.
- Some minor unification problems with apply/eauto discovered as well.
- Some places requiring more instances of Funext, as I expected.
Everything compiles quickly here.
Update submodule
Fix up some transparency issues
Remove an admit
More fixes
More minor changes
Remove more admits, add more work-arounds
Add back a space to minimize diff against master
Fix [simpl] going through abstract
[destruct] seems to not be working well...
Track Matthieu's trunk-polyproj branch
Update install with new branch