The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Interesting. It would be nice to be able to turn this discrimination of. In 
my concrete case  I needed to apply a general statement of the form

Theorem A (T:Type)(P:T->Type) : Q (sigT P).

to a type defined as 

Record B (T0:Type) : Type :=  bpair {bx:T0; by: R T0 bx}. 

as A T0 (fun x:T0 => R T0 x)

and had to re-write  quite a bit of code to replace all the "record" 
definitions by sigT's.

Vladimir.




On Feb 17, 2010, at 11:17 AM, Adam Chlipala wrote:

> Vladimir Voevodsky wrote:
>> They should be equal because they translate into the same terms in the 
>> calculus of inductive constructions.
> 
> The crucial fact here is that Coq is based on Gallina, not the literal CIC. 
>  Gallina has datatype generativity, just like ML does.