The Coq mailing list

[Guillaume Brunerie <guillaume.brunerie AT gmail.com>]

Le 18 avril 2012 11:48, Andrej Bauer <andrej.bauer AT andrej.com> a écrit :

Thank you for quick answers.

Frederic writes:
>> Inductive Q (x : A) : A ->  Type := horn : Q x x.
> The "problem" seems to be here already since, for Coq, Q has type A->A->Prop instead of A->A->Type as written
> explicitly.

But I explicitly require that Q map to Type... I see now that Coq is
lying to me, because "Print Q" leads me to believe that Q maps into
Type (it says "Inductive Q (x : A) : A -> Type :=  horn : Q x x"),
whereas

Parameter a : A.
Check (Q a).

tells me that Q a is in Prop. Can I force Q to map into Type somehow,
perhaps by using another layer of indirection?

> As far as homotopy type theory goes, as long as you don't mention Prop explicitely (which coerces inductive into > doing some kind of squashing, hence going beyond the power of MLTT+univalence), you can ignore Prop safely.

I find this hat do believe, not to mention it is very non-Coq-like. My
options seem to be:

(a) use the old definition of paths, which does not support rewriting.
(b) "trust" Coq and Prop.
(c) buy someone a beer to change Coq so it does not do this (the best
would be to make it configurable, I suppose).

I am in favor of (c) because the HoTT people might be the only ones
who really care about the issue. Vladimir Voevodsky's Foundations
patches don't seem to address this issue, or am I wrong?

They do, the patch "inductive-indices-level-matter-8.3.patch" address precisely this issue. But as Arnaud says, with this patch the standard library of Coq may not compile, but for HoTT you probably don’t need/want Coq’s standard library anyway.
For more information about this and about how to compile Coq without the standard library, see the READMEs here

https://github.com/vladimirias/Foundations
https://github.com/vladimirias/Foundations/tree/master/Coq_patches

Best regards,

Guillaume

With kind regards,

Andrej