# An axiom for John Major's Equality

In the the standard library of Coq, there is the axiom:

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


Why isn't it provable? Can it be reduced to more elementary axioms? Is it consistent with impredicative Set? Is there the same axiom in Agda?

• The axiom can be proved with Streicher's K. See e.g. axioms.v file from fcsl-pcm library by Aleks Nanevski. There is no direct proof of the axiom in the form you stated, but it can be done with the help of dynE lemma at the end of the linked file. Mar 15, 2019 at 16:48
• @AntonTrunov What is the idea of the proof starting from Streicher's K?
– Bob
Mar 15, 2019 at 17:08
• We know that Streicher's K is equivalent to Invariance by Substitution of Reflexive Equality Proofs (see EqDepFacts.v) an this last one implies the injectivity of the projection of the dependent pair (called inj_pair2 in Coq). From JMeq_eq x y follows existT id A x = existT id A y and using inj_pair2 we get x = y. Mar 15, 2019 at 20:55
• There is also a homotopy type theory explanation: homotopytypetheory.org/2012/11/21/on-heterogeneous-equality
– cody
Mar 16, 2019 at 2:04
• In Agda (or by using Equations), you can prove it using dependent pattern matching, which is itself equivalent to Streicher's K (there is a limited form of DPM available even without assuming K, but not enough to prove JMEq_Eq).
– xrq
Mar 18, 2019 at 20:09