The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

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.