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?

  • 2
    $\begingroup$ 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. $\endgroup$ Mar 15, 2019 at 16:48
  • $\begingroup$ @AntonTrunov What is the idea of the proof starting from Streicher's K? $\endgroup$
    – Bob
    Mar 15, 2019 at 17:08
  • 1
    $\begingroup$ 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. $\endgroup$ Mar 15, 2019 at 20:55
  • 2
    $\begingroup$ There is also a homotopy type theory explanation: homotopytypetheory.org/2012/11/21/on-heterogeneous-equality $\endgroup$
    – cody
    Mar 16, 2019 at 2:04
  • 1
    $\begingroup$ 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). $\endgroup$
    – xrq
    Mar 18, 2019 at 20:09


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.