# Proving uniqueness of identity proofs from J

by

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.

Tweet this Top

## License

This work (Proving uniqueness of identity proofs from J) is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Create an issue to apply for commentary