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.