The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

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?

With kind regards,

Andrej