8
$\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?

Improve this question
$\endgroup$
5
  • 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 '19 at 16:48
  • $\begingroup$ @AntonTrunov What is the idea of the proof starting from Streicher's K? $\endgroup$ – Bob Mar 15 '19 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 '19 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 '19 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 '19 at 20:09
1
$\begingroup$

I'll try to explain this without mentioning "K" or "UIP". Here's a proof in Coq -- unfortunately, it uses JMeq_ind (it is supposed to be the eliminator/induction principle of JMeq) which is based on JMeq_eq:

Require Import Coq.Logic.JMeq.

Definition JMeq_eq2 : forall (A : Type) (x y : A),
  JMeq x y -> x = y.
Proof.
  intros A x.
  apply (JMeq_ind (x := x) (fun a => x = a)).
  reflexivity.
Qed.

This is consistent with impredicative Set (citation needed -- this is just a guess). Under the default setting of Agda, you can prove it (JMeq in Agda is ≅) as wel:

open import Relation.Binary.PropositionalEquality
open import Relation.Binary.HeterogeneousEquality

JMeq-eq : (A : Set) (x y : A) -> (x ≅ y) -> x ≡ y
JMeq-eq A x y refl = refl

However, this works only because Agda by default enables --with-K mode (if you don't understand what is K, don't worry), which have less restrictions to the pattern matching as well as definitions of inductive types. Agda will reject the simplest definition (say, no universe polymorphism) of JMeq if we enable --without-K explicitly (this simply disable --with-K. Coq is under this mode by default):

{-# OPTIONS --without-K #-}

infix 4 _≅_
data _≅_ {A : Set} (x : A) : {B : Set} → B → Set where
   refl : x ≅ x

The way Agda rejects it is by restricting the level of indices, they need to have lower level than the inductive type itself:

Set₁ is not less or equal than Set
when checking the definition of _≅_

If you want a universe in the indices under --without-K, you need to explicitly make the level of B less than A (so you have to do something like data _≅_ {A : Set (suc l)} (x : A) : {B : Set l} → B → Set (suc l)), which makes x (which is an instance of A) an invalid instance of type B. Agda has to do this because it will automatically generate a "≅_ind" if you can define ≅, and we call it dependent pattern matching.

In Coq, universe polymorphism is automatically resolved by the compiler, so this trick won't work in Coq. I think Coq simply don't have an eliminator for JMeq built-in, so the situation is similar to Agda with the restrictions.

Improve this answer
$\endgroup$
4
  • $\begingroup$ "This is consistent with impredicative Set." Do you have a reference for that? $\endgroup$ – cody Sep 23 '20 at 14:46
  • $\begingroup$ If you have impredicativity (can be simulated in Agda by --type-in-type) and even you don't have K built-in you can prove it, I suppose. So, this is my assumption. Correct me if I'm wrong, I'd be happy to fix my mistake! :) $\endgroup$ – ice1000 Sep 23 '20 at 16:28
  • $\begingroup$ I mean, --type-in-type by itself is inconsistent already even --without-K. $\endgroup$ – cody Sep 23 '20 at 20:56
  • $\begingroup$ That being said, I don't know whether K is inconsistent with impredicative sets "a la" Coq. I suspect it is consistent, I just don't know of a good reference for a proof. Maybe Termination of rewriting in the Calculus of Constructions by DARIA WALUKIEWICZ-CHRZĄSZCZ, but I'd have to check. $\endgroup$ – cody Sep 23 '20 at 21:05

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.