The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

They should be equal because they translate into the same terms in the 
calculus of inductive constructions (up to the universe variables, but that 
should just produce some additional constrains on universes when Lemma a is 
processed). In fact the following does not work either and here there are no 
issues with universes:

Inductive b1:Set := b10: b1| b11: b1.
Inductive b2:Set := b20: b2| b21: b2.

Lemma a: b20 = b10.


On the other hand the following works just fine:


Variable T:Type.
Definition A:Type := forall a:T, T.
Definition B:Type := forall b:T, T.
Lemma c: forall a:A, forall b:B, a=b. 

and so should the first example. 

Vladimir.





On Feb 17, 2010, at 10:08 AM, Adam Chlipala wrote:

> Vladimir Voevodsky wrote:
>> Inductive total2 (T:Type) (P:T ->  Type) := tpair: forall t:T, forall x: P 
>> t, total2 T P.
>> 
>> Inductive total2' (T:Type) (P:T ->  Type) := tpair': forall t:T, forall x: 
>> P t, total2' T P.
>> 
>> Definition pr21 (T:Type) (P:T ->  Type) (z: total2 T P) : T :=
>> match z with
>> tpair t x =>  t
>> end.
>> 
>> Lemma a (T:Type)(P:T->Type)(z: total2' T P) : pr21 T P z.
>> 
>> 
>> Coq does not understand the lemma saying that z has to be of type total2 T 
>> P. However, total2 T P and total2' T P are equal (up to alpha equivalence) 
>> as the terms of the calculus of construction and the membership in one is 
>> the same as in another. How can I point it out to Coq?
>>   
> 
> You can write conversion functions between them, and you can even get these 
> functions applied automatically as coercions.  I don't think there's any 
> way to prove that these types are equal in the sense of [=], though.  The 
> standard model shows that it would be OK to add that as an axiom, as long 
> as you don't have some other especially exotic (and contradictory) axiom 
> around.