6
$\begingroup$

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?

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.