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.
But why the:

Axiom dummy_funext_type : Type.



On Wed, Jul 23, 2014 at 4:26 PM, Jason Gross <notifications@github.com>
wrote:

> In theories/Overture.v:
>
> > @@ -347,8 +347,11 @@ Hint Extern 0 => progress change Contr_internal with Contr in * : typeclass_inst
> >  (** *** Function extensionality *)
> >
> >  (** The function extensionality axiom is formulated as a class. To use it in a theorem, just assume it with [`{Funext}], and then you can use [path_forall], defined below.  If you need function extensionality for a whole development, you can assume it for an entire Section with [Context `{Funext}].  *)
> > -Class Funext :=
> > -  { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
> > +(** We use a dummy class and an axiom to get universe polymorphism of [Funext] while still tracking its uses. *)
> > +Axiom dummy_funext_type : Type.
>
> Done. Here's the elaborated comment:
>
> We use a dummy class and an axiom to get universe polymorphism of Funext
> while still tracking its uses. Coq's universe polymorphism is parametric;
> in all definitions, all universes are quantified over before any other
> variables. It's impossible to state a theorem like (forall i : Level, P
> i) -> Q (e.g., "if C has all limits of all sizes, then C is a preorder"
> isn't statable).¹ By making isequiv_apD10 an Axiom rather than a
> per-theorem hypothesis, we can use it at multiple incompatible universe
> levels. By only allowing use of the axiom when we have a Funext in the
> context, we can still track what theorems depend on it (because their type
> will mention Funext).
>
> ¹ That's not technically true; it might be possible to get non-parametric
> universe polymorphism using Modules and (Module) Functors; we can use
> functors to quantify over a Module Type which requires a polymorphic
> proof of a given hypothesis, and then use that hypothesis polymorphically
> in any theorem we prove in our new Module Functor. But that is far beyond
> the scope of this file.
>
> (Except I used * rather than ¹ for the footnote in the source.)
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/415/files#r15290280>.
>