The Coq mailing list

[Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>]

On 22 Sep 2010, at 19:11, Bruno Barras wrote:

> don't know what you mean by "parametricity of Coq's logic". It is true that 
> you cannot do some case-analysis on objects in Type, but dependent types 
> and the complex language on types will not give you the same "theorems for 
> free" as for system F...

Free theorems should also work for Coq, but the principle he wanted (all type 
functions are constant) isn't one of them. Chad Brown gave a very nice and 
short proof that it is unsound. 

Cheers,
Thorsten