Proving uniqueness of identity proofs from J

2020, Aug 15 by Tesla Ice Zhang

I’m writing this post to demonstrate an attempt to prove uip from J, and analyze why is it not possible.

{-# OPTIONS --with-K #-}
{-# OPTIONS --allow-unsolved-metas #-}
module 2020-8-15-AxiomK where

This article assumes basic dependently-typed programming and (a very vague impression is enough) some basic HoTT. It would be good if you know the story behind Agda’s --without-K, but it’s not necessary.

open import Agda.Primitive
import Agda.Builtin.Equality as Equality

In this article, I will use the term “equality type” and “identity type” interchangeably.

private
  variable
    a b : Level
    A : Set a

Normal inductive types

module BeforeWeStart where
  open Equality

Before we get started, let’s look at some normal inductive types. For simplicity, I’ll pick the ⊤ type. It’s already predefined in Agda builtin library:

  open import Agda.Builtin.Unit

We can click on the following reference to see its definition:

  --  ↓ click me
  _ = ⊤
  --  ↑ click me

Its elimination rule is simple, which is effectively the pattern matching principle of ⊤, and as you can see we can define it in terms of pattern matching:

  ⊤-elim : (P : ⊤ → Set b) → P tt → (t : ⊤) → P t
  ⊤-elim P p tt = p

Then, we can also prove a uniqueness rule in terms of the elimination rule:

  ⊤-unique : ∀ t → t ≡ tt
  ⊤-unique = ⊤-elim (_≡ tt) refl

The P parameter of ⊤-elim is named as motive though I have no idea who used this name first. Using the eliminator requires an explicit motive to be provided, while pattern matching don’t:

  ⊤-unique′ : ∀ t → t ≡ tt
  ⊤-unique′ tt = refl

This subtle difference leads to a lot of confusion when the motive causes some problems and it messes pattern matching up. The problem comes from some certain indexed inductive types, revealed most clearly in the identity type.

The identity type – less restricted

So, what is the identity type? Well, we’ve already used it in the statement of ⊤-unique, but I haven’t talked about its definition. Let’s do it now.

module WorkingProof where

If we define the identity type as used in (the paper is titled “Eliminating Dependent Pattern Matching”) GMM06, it’ll look like the following:

  infix 4 _≅_

  data _≅_ {A : Set a} (x : A) : {B : Set b} → B → Set a where
    refl : x ≅ x

This is also the definition of the = type constructor in Idris.

A little explanation of this definition: we’ve defined an inductive type ≅, which has two value parameters – one of type A, and one of type B. So, given term 1 of type Nat, true of type Bool, we can state that 1 ≅ true is a type:

  open import Agda.Builtin.Nat
  open import Agda.Builtin.Bool

  _ : Set
  _ = 1 ≅ true

We can define its eliminator, which is also named as the J rule for historical reason due to Per Martin-Löf:

  J : {x : A} (P : (y : A) → x ≅ y → Set b) →
      P x refl → (y : A) (x≡y : x ≅ y) → P y x≡y
  J P p ._ refl = p

The motive this time is a little bit longer, but it’s structurally similar to ⊤-elim, so I’ll consider it readable.

We can prove the uniqueness principle:

  uip : {x : A} (p : x ≅ x) → refl {x = x} ≅ p
  uip refl = refl

To better inspect the proof, we can prove uip in terms of J:

  uip′ : {x : A} (p : x ≅ x) → refl {x = x} ≅ p
  uip′ = J (λ x → refl {x = x} ≅_) refl _

This result is very normal and very old. It looks trivial because you can say:

I have a datatype with a single constructor, so by canonicity we will always have a term of type x ≅ y for any value x and y reduced to WHNF refl, even if x and y are equal to each other. What’s the problem?

This fact is even clearer if you simply compare ≅ with ⊤. The ≅ type is just a more restricted version of ⊤, where the only difference is just an index.

How do we like ≅?

Well, we can also see some downsides of this definition of the equality type: it doesn’t require both sides to have the same type. Say, if we wanna write refl ≅ p, we cannot infer the implicit parameters of LHS refl because we do not know its type (even though we know RHS p’s type). This is why I’m annotating the implicit argument explicitly, all the time in uip and uip′.

However, it is also good because it’s very flexible. For instance, we can state 1 ≅ true, where the two sides are of different types. Sometimes types don’t simply get syntactic equality, like in case a : Vec (n + m) A and b : Vec (m + n) A, you need to have such flexibility to state that a ≅ b to be a valid type.

Since the two sides can have different types, we often refer to this type as the heterogeneous equality type.

So you might wanna ask,

But how about homogeneous equality?

module CannotProve where

Well, the homogeneous (opposite to heterogeneous) equality type is preferred in Agda. So, it’s made builtin.

  open Equality

We can click on the following reference to see its definition:

  --   ↓ click me
  _ = _≡_
  --   ↑ click me

The difference between ≡ and ≅ is subtle – it requires the terms on two sides to have the same type. So, 1 ≡ true and the Vec example discussed above won’t type-check.

We can definitely prove its elimination principle:

  J : {x : A} (P : (y : A) → x ≡ y → Set b) →
      P x refl → (y : A) (x≡y : x ≡ y) → P y x≡y
  J P p ._ refl = p

The proof is (almost) identical to J of ≅. Note that from now on we’re going to use J instead of pattern matching so we can see the motive explicitly.

However, when we’re coming to a proof of uip on ≡, things become unpleasent. The original proof won’t typecheck, so putting it here directly will block the compilation of this blog. So, I made the motive a goal so it typechecks but gives some warnings.

  uip′ : {x : A} (p : x ≡ x) → refl {x = x} ≡ p
  uip′ = J(λxx→{!refl {x = xx} ≡_!})refl_

Since it typechecks under a heterogenous setting, we can tell that the motive contains an equality type expression whose two sides are of the same type. If we try to fill the goal we get the following error message, which tells us which expression is causing the problem:

x != xx of type A
when checking that the expression section has type xx ≡ xx

This error contains very little information, so not very helpful. It even talks about section which I have no idea what it is. And if we leave the code untouched the warnings are as follows (you have to remove the --allow-unsolved-metas flag to see the errors below):

?0 : x ≡ xx → Set A.a
_A_144 : Set A.a  [ at 2020-8-15-AxiomK.lagda.md:252,42-46 ]
_x_145 : _A_144  [ at 2020-8-15-AxiomK.lagda.md:252,42-46 ]

———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
  _x_145 ≡ _x_145 =< ?0 (xx = x) refl (blocked on _142)
  ?0 (xx = x) x≡y =< refl ≡ x≡y (blocked on _142)

This time it’s much better. We can see that the motive takes xx : A and p : x ≡ xx, same as the motive of J of ≅. However, the left hand side is refl {x = xx}, which is of type xx ≡ xx. So, Agda wants to unify these two types and it finds the RHS of both types are the same. This is why the same code works under heterogenous equality, and it also explains the error message!

Then, we may start thinking: is it possible to change the motive to make it work? Well, since we want to state the theorem that refl ≡ p, we need to make p of type xx ≡ xx. In the error message, we see that Agda wants the motive, as a function, to return refl ≡ x≡y when applied by x≡y. So, we cannot pattern match on the argument (otherwise this application will stuck). In other words, we cannot eliminate p, but we need to show that p is of type xx ≡ xx. In order to do so, we need to show that p is equal to refl. This is exactly what we’re doing right now. So, the proof is circular.

This unprovability is the result of “A groupoid model refutes uniqueness of identity proofs” by Martin Hofmann and Thomas Streicher. A PDF copy I have found is here. The paper explained such result in a categorical point of view, though.

Conclusion

That’s how you cannot derive uip from J, not to mention the equivalent (proved in theorem 7.2.1, the HoTT Book) (though looks more general) version K. So, ideally, we should have a type theory where K is an optional theorem and can be disabled.

Thanks to @InanimateDream_ (twitter allows username renamings, so it’s pointless to put a link here) for discussing this proof with me last year.

Initially, this inability to prove uip does not sound right to me because ultimately you have only one constructor of ≡, so by canonicity you should be able to prove uip. I may talk more about this fact with indexed inductive types and HoTT in some upcoming post, stay tuned.