HEq and Axiom K: An Exploration in Lean

While reading Conor McBride's A Few Constructions on Constructors, I came across his definition of Heterogeneous Equality (represented here using Lean axioms):

He also introduced a special elimination rule:

Notice the crucial difference in this special recursor: its motive forces the type of the second index, b, to match α.

The author then mentions that heterogeneous equality—when equipped with this special eliminator—is exactly as strong as homogeneous equality plus Axiom K. The construction involves representing heterogeneous equality as homogeneous equality over sigma types. In this framework, the implication (Σ α, x : α) = (Σ α, y : α) → x = y is equivalent to axiom K.

When I first read this, I was completely stumped. I realized that my understanding of equality recursors, Axioms J and K, and their relationship with heterogeneous equality was surprisingly shallow. I figured it would be an excellent exercise to manually derive in Lean how this special eliminator, combined with HEq, implies K. With my advisor's help, we finished this exercise. This post summarizes our proofs.

Note: Because Lean inherently supports Uniqueness of Identity Proofs (UIP), we must be extremely careful not to rely on it accidentally. This means we cannot use the cases tactic, nor can we use Lean's built-in Eq (=). Every operation must be implemented manually by invoking the rec function generated by our custom inductive types.

We start by defining a homogeneous equality with a universe level of at least Type:

We'll use the ≡ symbol to denote our custom homogeneous equality. For convenience, we also define subst and symm.

For heterogeneous equality, we will rely directly on Lean's built-in HEq (≍). As long as we avoid functions like eq_of_heq and refrain from using cases for dependent pattern matching, we are safe.

Let's add the special eliminator mentioned earlier:

Our ultimate goal is to prove K, or its equivalent, UIP:

Unlike Agda, K cannot simply be "disabled" in Lean. We must actively avoid using cases because it would immediately close this goal relying on UIP under the hood (we will look at what it actually generates later):

Before diving into the proof, let's map out our strategy. Directly obtaining z ≡ (Eq'.refl x) is tricky. We need a way to connect it to HEq so we can exploit that special eliminator.

We can start with the sigma type mentioned in the initial claim. As discussed in On Heterogeneous Equality, a sigma type is a pointed type, and heterogeneous equality is equivalent to homogeneous equality on pointed types. We can prove this using the universe-polymorphic PSigma (denoted here with Σ').

Without touching HEq.rec' yet, we have achieved a bidirectional conversion between heterogeneous equality and homogeneous equality on sigma types.

Now, consider our goal z ≡ (Eq'.refl x). Its heterogeneous counterpart, z ≍ Eq'.refl x, can be obtained by applying heq_of_sigma to ⟨x ≡ x, z⟩ ≡ ⟨x ≡ x, Eq'.refl x⟩. The Eq' of this sigma type can be then proven directly:

Here is the path we've established so far:

(z : x ≡ x)
------------- (sigma_eq)
⟨x ≡ x, z⟩ ≡ ⟨x ≡ x, Eq'.refl x⟩
------------- (heq_of_sigma)
z ≍ (Eq'.refl x)
------------- (???)
z ≡ (Eq'.refl x)

We are only one step away! Obviously, the missing link can be filled by eq_of_heq, but remember: we are strictly restricted to using recursors.

But here we hit a wall. The obvious elimination fails because the second index x' has type β, and heq : x ≍ x' cannot cast the type of x' to match x.

Finally, it is time to unleash that special eliminator for HEq:

Because the motive forces the second index to share a type with the first index, we successfully eliminate from HEq to Eq. Now we can close out the proof:

With UIP at our disposal, proving K is a breeze:

Conversely, K can also be used to prove UIP, confirming their equivalence:

Ultimately, the core contribution of this special eliminator is essentially eq_of_heq (known as JMeq_eq in Rocq), which we've just shown implies Axiom K.

Returning to the tactic-based proof for a moment, let's look at what Lean automatically did for us earlier:

def eq_uip'.{u} : {α : Sort u} → (x : α) → (z : x ≡ x) → z ≡ Eq'.refl x :=
fun {α} x z => Eq'.casesOn (motive := fun a t => x = a → z ≍ t → z ≡ Eq'.refl x) z (fun h h_1 => ⋯ ▸ Eq'.rfl) ⋯ ⋯

It generated quite a few extra proof terms. Simplified and cleaned up, it looks like this:

It appears Lean inserted an Eq proof relying on UIP directly into the motive's parameters, but it doesn't play a crucial role. We can actually simplify it even further:

As we can see, the core of the automated proof uses eq_of_heq to convert HEq to Eq, and then eliminates it using @Eq.rec. Try as we might to avoid it manually, Lean's automated machinery strictly and inevitably relies on UIP.