The Coq mailing list

[Michael Shulman <mshulman AT ucsd.edu>]

On Thu, Apr 19, 2012 at 05:24, Guillaume Brunerie
<guillaume.brunerie AT gmail.com>
 wrote:
> But as Arnaud says, with this patch the standard
> library of Coq may not compile,

I believe Vladimir's email in March said that the hanging of the
standard library is due to a different patch.  (I haven't tried any of
these patches myself except for type-in-type.)  If it's true that the
inductive-indices-level-matter patch (also) breaks the standard
library, I am curious to know why?  Would it work if one simply
changed some "Type"s in the standard library to "Prop"s?

But what I would really like to know is, would it be possible to have
this patch included in the main Coq trunk, perhaps enabled or disabled
by a flag?  If I understand things correctly, the issue is about how
Coq parses our source code into an internal representation -- i.e.
what internal universe level it assigns when we write "Type" -- which
makes it sound to me as though there would be no problem mixing
*compiled* code that has this behavior turned on or off.  (If that's
not the case, then maybe what I'm asking for would be more difficult,
but I would still like to request it.)  That way the standard library
or other code could be compiled with the current behavior, if they
really need it for some reason (why?), but homotopy type theorists
could turn on the modified behavior for our purposes.

I would also like to ask the same thing about the type-in-type patch
which makes Coq formally inconsistent.  At least until someone has the
time to implement real universe polymorphism (would such an
implementation be accepted for the main trunk if offered?).

I and many others are working hard to get people interested in
homotopy type theory, and I think Coq is currently the best way to do
homotopy type theory.  If I may put on a salesman hat for a minute (-:
I think rising interest in homotopy type theory is bound to generate
more interest in type theory more generally as a foundational system,
and in proof assistants like Coq -- so the type theory community
stands to benefit from this even if you don't care about homotopy as
such.  But having to patch and recompile Coq oneself is a significant
barrier to entry that I would prefer not to have to ask of potential
homotopy type theorists.

Best,
Mike