The Coq mailing list

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

>>
>> I find this hat do believe, not to mention it is very non-Coq-like.
>
> I don't understand why. This is what singleton elimitation does.

What I find hard to believe is that I can ignore Prop safely when I
work on HoTT and Coq secretly introduces Prop. How do I know it's not
going to do some proof-irrelevanty thingy?

>> (c) buy someone a beer to change Coq so it does not do this (the best
>> would be to make it configurable, I suppose).
>
> Well, that may require a mightier bribe than that, and a more secure
> position for yours truly. But it's not impossible either. Bear in mind that
> it would require a serious incompatibility with existing libraries as
> propositional equality would not support rewriting (at least not always).

I am not proposing an incompatibility change, I think. I am proposing
that the type should be honored when explicitly given. Because I
explicitly defined that Q should map to Type, it should map to Type.
If I asked Coq to _infer_ the type and it decided it was Prop, then I
would have no objection. But as far as I am concerned this is a bug.
If I define

Definition cow : Bovine := ....

then cow should be Bovine and not something else. I am tempted to file
a bug report.

With kind regards,

Andrej