# How does the elimination rule of the heterogeneous equality type imply a weak version of K?

A heterogeneous equality type has the former $$\cfrac{\Gamma\vdash A~\texttt{type} \quad \Gamma\vdash B~\texttt{type} \quad \Gamma\vdash a:A \quad \Gamma\vdash b:B}{\Gamma\vdash a\simeq b~\texttt{type}}$$ with the reflexivity introduction rule and a J-like elimination rule.

This is confusing because like in Agda, the --without-K option refutes that may lead to K (so you can't even define the heterogeneous equality type). If we do not use the option, we can't tell where exactly the heterogeneous equality type contributes to the construction of K.

• Wouldn't this question be phrased more clearly if it didn't mix type theory and command-line options of Agda? Why not just speak about Axiom K instead of saying things like "disable builtin K"? Commented Feb 10, 2022 at 23:07
• It would be helpful to state the elimination rule here Commented Feb 11, 2022 at 3:16
• And what would be even better is substantiation of the claim given in the title, namely that hetereogenous equality implies (a version of) axiom $K$. How is that the case? Commented Feb 11, 2022 at 6:47
• I found a reference for the heterogenous/K claim: "Elimination with a Motive" by Conor McBride, chapter 3. And chapter 5.1.3 of Conor McBride's thesis "Dependently Typed Functional Programs and their Proofs". Commented Feb 11, 2022 at 11:24
• I also don't understand. John Major Heterogeneous Equality in CCHM doesn't need K. Commented Feb 12, 2022 at 1:29

I looked at the thesis mentioned by Labbekak. The relevant section is 5.1.3. The situation goes like this...

First, you can use $$J$$ to prove 'heterogeneous uniqueness of identity proofs'. That goes like so in Agda:

data JM {A : Set ℓ} (a : A) : {B : Set ℓ} → B → Set (Level.suc ℓ) where
refl : JM a a

jmk : ∀(a : A) → (p : a ≡ a) → JM p {a ≡ a} refl
jmk a p = J (λ b q → JM q {a ≡ a} refl) p refl


The usual stumbling point is that the family there is not well typed, because $$q : a = b$$, but that doesn't matter for $$\mathsf{JM}$$.

However, the thing the thesis points out is that it is not using the inductive eliminator for $$\mathsf{JM}$$. That only allows eliminating into a family like (switching to $$\simeq$$):

$$P : (B : \mathcal{U}) → (b : B) → a \simeq b → \cal U$$

Where $$A : \cal U$$ and $$a : A$$ are ambient. Instead, it uses an eliminator into families of the form:

$$P : (b : A) → a \simeq b → \cal U$$

Importantly, the homogeneous identity type is a family like this, so it allows us to write a function $$a \simeq b → a = b$$ that would be impossible to write with the inductive eliminator. So, this lets us turn 'heterogeneous uniqueness of identity proofs' into uniqueness of identity proofs:

JMJT =
∀{c ℓ} {A : Set ℓ} {a : A}
→ (P : (b : A) → JM a b → Set c)
→ P a refl
→ {b : A} (p : JM a b) → P b p

module _ (JMJ : JMJT) where
jme : ∀{a b : A} → JM a b → a ≡ b
jme {a = a} = JMJ (λ b _ → a ≡ b) refl

ulp : ∀{a : A} → (p : a ≡ a) → p ≡ refl
ulp p = jme (jmk _ p)


Note that Agda doesn't allow you to implement $$\mathsf{JMJ}$$ when axiom K is turned off.

If you think about what this means from a HoTT perspective, the fact that $$P$$ is parameterized by $$B$$ in the genuine inductive eliminator is (I think) the extra degree of freedom needed for it to be a, "dependent path." $$\mathsf{jmk}$$ is just the dependent path corresponding to a square like:

         p
a -------- b
|          |
p |          | refl
|          |
b -------- b
refl


(or possibly some other variation) But, the restricted eliminator corresponds to the assumption that every dependent path (that begins and ends in $$A$$) lies over the reflexive path on $$A$$, and that is how axiom K gets introduced.

Of course, this means that heterogeneous equality is not inherently related to axiom K at all. But, it's rather easy to see how people could be confused about the nuances. That is, for homogeneous equality, axiom K:

$$(P : a = a → \mathcal{U}) → P\ \mathsf{refl} → ∀ e → P\ e$$

is equivalent to uniqueness of identity proofs:

$$(e : a = a) → e = \mathsf{refl}$$

However, for heterogeneous equality:

$$(e : a \simeq b) → e \simeq \mathsf{refl}$$

is an obvious theorem about commutative squares, and is not equivalent to axiom K:

$$(P : a \simeq a → \mathcal{U}) → P\ \mathsf{refl} → ∀ e → P\ e$$

PS: I guess one thing to note is that the "John Major" reference is all about the different eliminator. So, normal inductively defined heterogeneous equality with the proper inductive eliminator (and without axiom K) is not "John Major equality."

PPS: One other thing occurred to me. The inductive heterogeneous equality is not precisely equivalent to the 'dependent paths' in the HoTT book or cubical theories because it is only indexed by the end points of the type paths. It is actually like $$Σ_{P: A = B}\ \mathsf{transport}_P\ a = b$$. The thesis calls the inductive one "useless," and it might be on target even in a homotopy context, because we usually want to talk about paths lying over a specific $$P$$. For instance, in a univalent scenario, we have $$\mathsf{false} \simeq \mathsf{false}$$ and $$\mathsf{false} \simeq \mathsf{true}$$, because the reflexive equivalence $$\mathsf{Bool} = \mathsf{Bool}$$ gives the first fact, and the swapping equivalence gives the second. So, this particular inductive definition is not useful for the same purposes as homogeneous equality without K.