Move to trunk

The day we've all been waiting for has arrived.  The days of faster Coq'ing are upon us.  This pull request updates the library with the last remaining changes necessary to move to trunk.

If you make use of the bundled submodule for building Coq, It is very likely that you will have to run `./autogen.sh` after pulling (and, of course, re-build Coq).

Since the `Local` keyword has been replaced by the `Private` keyword, this code will no longer compile with HoTT/coq.  If we want to, we can add a tag to the HoTT/coq version for posterity.

In this pull request, I've used an `admit` so as not to depend on #407.  I'm happy to have either this or #407 merged first (with a slight preference for #407 first), and will rebase the other one to be compatible.

Once this is merged, and the troubles with primitive projections are fixed, I'll submit a pull request to take advantage of primitive projections and eta.

This will allow us to deal with #335 and #402.  This closes #301.
Provided you want to use a name (H0), I would choose `fs` instead of `H0`.


On Wed, Jul 23, 2014 at 4:10 PM, Jason Gross <notifications@github.com>
wrote:

> In theories/categories/NaturalTransformation/Composition/Laws.v:
>
> > @@ -52,7 +52,7 @@ Hint Rewrite @left_identity @right_identity : category.
> >  Hint Rewrite @left_identity @right_identity : natural_transformation.
> >
> >  Section whisker.
> > -  Context `{fs : Funext}.
>
> I stripped the fses because you should never be mentioning them by name.
> (I inserted H0 because I want H as a natural transformation.) Even though
> we should never use the Funext by name, do you think I should go back to
> fs?
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/415/files#r15289348>.
>