Define Modality, prove that double negation is one
Add a dependent version of minus1Trunc_map
Do Exercise 7.1 from the book
Add many variants of the [simpl rewrite] tactic

It's unfortunate that Coq doesn't give us a notation of saying "this
takes anything that rewrite can take".  But these are useful for
making tactic scripts conceptually clearer.
Add some theorems about equivalence of equiv and iso in set_cat
Use a debian repository for HoTT/coq

Edward Yang (@ezyang) helpfully packaged HoTT/coq a while back.  The
category theory is getting slow enough that the build that generates the
html periodically fails, and I have to kick travis.  This should buy us
another 5-10 minutes.

Also install libcoq-ocaml-dev
Add the -no-native-compiler argument to coqtop

It's required for a Coq built without that argument to not complain
about various things.
Merge pull request #351 from JasonGross/ex-7-1

Exercise 7.1
I am merging as this is a small change which does not seem very critical.
Please let me know if this is too quick.
Merge pull request #355 from JasonGross/more-rewrite

Add many variants of the [simpl rewrite] tactic

Merging, this seems like harmless notation.
Define a variant of [path_sigma] for hprops

In this case, we don't need to provide the second projection.

Also prove that it's an equivalence.

Also move [equiv_path_sigma_hprop] to HProp.v, because it fits there,
and fits in nicely with the proof.
Robustify isequiv_path_sigma_hprop
Merge pull request #358 from JasonGross/use-ppa

Use a debian repository for HoTT/coq
Merge pull request #352 from JasonGross/ex-7-12

Define Modality, prove that double negation is one
Merge pull request #354 from JasonGross/sigma-hprop

Define a variant of [path_sigma] for hprops.
Merge pull request #357 from JasonGross/set-cat-morphisms

Add some theorems about equivalence of equiv and iso in set_cat
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