<p>In the the standard library of Coq, there is the axiom:</p>

<pre><code>Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -&gt; x = y.
</code></pre>

<p>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?</p>

CC BY-SA 4.0
2019-03-15T16:48:11.483Z
The axiom can be proved with Streicher's K. See e.g. [axioms.v](https://github.com/imdea-software/fcsl-pcm/blob/master/pcm/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.
Anton Trunov
CC BY-SA 4.0
2019-03-15T17:08:42.977Z
@AntonTrunov What is the idea of the proof starting from Streicher's K?
Bob
CC BY-SA 4.0
2019-03-15T20:55:45.190Z
We know that Streicher's K is equivalent to Invariance by Substitution of Reflexive Equality Proofs (see [EqDepFacts.v](https://coq.inria.fr/distrib/current/stdlib/Coq.Logic.EqdepFacts.html)) 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`.
Anton Trunov
CC BY-SA 4.0
2019-03-16T02:04:16.880Z
There is also a homotopy type theory explanation: https://homotopytypetheory.org/2012/11/21/on-heterogeneous-equality/
cody
CC BY-SA 4.0
2019-03-18T20:09:39.017Z
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
CC BY-SA 4.0
2021-05-21T17:51:51.730Z
Here's a [discussion](https://ieeexplore.ieee.org/document/316071/) on the invalidity of K
ice1000
<dependent-type><coq><proof-theory><calculus-of-constructions><agda>
An axiom for John Major's Equality
Bob
# An axiom for John Major's Equality

(Asked by: username_0 on 2019-03-15)

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?

**Tags:** dependent-type, coq, proof-theory, calculus-of-constructions, agda

> **Comments:**
> **username_1**: The axiom can be proved with Streicher's K. See e.g. [axioms.v](https://github.com/imdea-software/fcsl-pcm/blob/master/pcm/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.  
> **username_0**: @AntonTrunov What is the idea of the proof starting from Streicher's K?  
> **username_1**: We know that Streicher's K is equivalent to Invariance by Substitution of Reflexive Equality Proofs (see [EqDepFacts.v](https://coq.inria.fr/distrib/current/stdlib/Coq.Logic.EqdepFacts.html)) 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`.  
> **username_2**: There is also a homotopy type theory explanation: https://homotopytypetheory.org/2012/11/21/on-heterogeneous-equality/  
> **username_3**: 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).  
> **username_4**: Here's a [discussion](https://ieeexplore.ieee.org/document/316071/) on the invalidity of K  

---

## 0 answers

