The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-sb.de>]

Hello

I have a question about the JMeq Library

It introduces the following axiom:

Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y.


In [1] McBride says that the elimination principles on can derive using
this axiom "give[s] exactly the same strength as Martin-Löfs equality
extended with Altenkirch and Streicher's 'uniqueness of identity proofs'
axiom."

So is JMeq_eq is provable in Coq using UIP? Does anyone have a proof?


-- 
Regards
Christian


[1] McBride, Elimination with a Motive, Proceedings of TYPES 2000, LNCS
2277, pp 197-216, 2002.