The Coq mailing list

[Cuihtlauac ALVARADO <cuihtlauac.alvarado AT francetelecom.com>]

Hi,

>  > Inductive myEq:(A,B:Type)A->B->Prop :=
>  >  myEq_refl: (C:Type)(x:C) (myEq C C x x).
> 
> This is known as John Major's  equality (the origin of this name is to
> be found  is C. Mc Bride's  PhD thesis), and  this is part of  the Coq
> standard library; see http://coq.inria.fr/library/Coq.Logic.JMeq.html

It's not exactly John Major equality, without Uniqueness of Identity
Proofs axiom you cannot prove Leibniz elimination for this equality :

  (A:Type)(P:A->Prop)(x,y:A)(myEq A A x y)->(P x)->(P y)

Conor will correct me if I'm wrong, but John Major equality is really
myEq + Leibniz Elimination (and regular elim of myEq to /dev/null).

In the end Leibniz elimination for myEq is equivalent to UIP.

>  > But I can't prove equivalence of myEq and eqT... Is it possible? If
>  > not, why? They both look as the smallest reflexive relation to me...
> 
> No, it is not provable.
> 
> However, Marco Maggesi recently  proved it assuming proof irrelevance.
> See http://www.math.unifi.it/~maggesi/coq/jmeq.v

It does not help much: PI => UIP

-- 
Cuihtlauac ALVARADO - France Telecom R&D - DTL/TAL
2, avenue Pierre Marzin - 22307 Lannion - France
Tel: +33 2 96 05 32 73 - Fax: +33 2 96 05 39 45