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.
