# Zulip Chat Archive

## Stream: new members

### Topic: heq to eq

#### Kyle Miller (Sep 20 2020 at 02:18):

Is the following provable? I suspect it isn't, but it would be nice to know one way or another.

```
inductive foo {α : Type} : α → Type
| mk (x : α) : foo x
example {α : Type} (x y : α) (h : foo.mk x == foo.mk y) : x = y :=
begin
sorry
end
```

#### Mario Carneiro (Sep 20 2020 at 03:24):

No it is not

#### Mario Carneiro (Sep 20 2020 at 03:37):

Here is a proof that it is consistently false:

```
def foo {α : Type} (x : α) : Type := unit
def foo.mk {α : Type} (x : α) : foo x := ()
def foo.cases_on {α : Type} {C : Π (a : α), foo a → Sort*} {a : α}
(n : foo a) (H : Π (x : α), C x (foo.mk x)) : C a n :=
by cases n; exact H a
theorem foo.beta {α : Type} {C : Π (a : α), foo a → Sort*} (a : α)
(H : Π (x : α), C x (foo.mk x)) : foo.cases_on (foo.mk a) H = H a := rfl
theorem not_foo_inj : ¬ ∀ {α : Type} (x y : α) (h : foo.mk x == foo.mk y), x = y
| H := by { cases H tt ff _, refl }
```

#### Kyle Miller (Sep 20 2020 at 03:58):

Thanks for the proof! This suggests that Reid's technique for heterogeneous equality (https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/heq.20alternative/near/210378589) is strictly better for types with indices in some contexts. In the example it was just `vector`

, and you can recover the length of a vector from one of its terms, but there are other inductive types like

```
inductive path {α : Type} (r : α → α → Prop) : α → α → Type
| nil {x : α} : path x x
| cons {x y z : α} (h : r x y) (p : path y z) : path x z
```

where being able to derive equalities on indices can be important. It seems your proof should carry over to two `nil`

entries being `heq`

not necessarily having equal `x`

values.

#### Mario Carneiro (Sep 20 2020 at 04:29):

Why would you want to compare `nil`

entries on different basepoints?

#### Mario Carneiro (Sep 20 2020 at 04:33):

I think it is best to pretend that heq doesn't exist. A type equality is sort of incomplete, because it contains the "elements are equal" part predicated on "indices are equal" that is not provided. Instead, as in that question, whenever you want to compare elements of different types you should tuple them up with the relevant indices to make it a homogeneous equality (not in Type). In the case of `path`

, that would be the type `\Sigma x y, path x y`

#### Mario Carneiro (Sep 20 2020 at 04:34):

Note that `<x, x, nil> = <y, y, nil> -> x = y`

is provable

#### Kyle Miller (Sep 20 2020 at 04:43):

One motivation for this question was to check I wasn't missing anything with `heq`

-- it seemed very underpowered and so, mostly out of curiosity, I asked this question. In the meantime, I've been using `\Sigma x y, path x y`

for equalities (well, I was first using Ried's method, but some universe variable considerations eventually made me move to sigma types, which you'd mentioned in the thread). The reason this came up was that I have two different ways of representing paths, and I wanted to show that they were equivalent. The composition of maps between these representations ends up with types that aren't definitionally equal to the original type (though they are equal) so I spent some time fruitlessly trying to get `heq`

to work before thinking that it might not actually be provable.

It would be kind of cool if there were a `heqi`

, heterogeneous equality with indices, that could be automatically derived, perhaps given some subset of indices for a given inductive type.

#### Kenny Lau (Sep 20 2020 at 06:48):

Can we add an axiom `\forall (x : A) (y : B) (h : x == y), A = B`

?

#### Kyle Miller (Sep 20 2020 at 06:51):

Isn't that `type_eq_of_heq`

?

#### Kyle Miller (Sep 20 2020 at 06:52):

I don't know the type theory, other than the proof Mario gave, but it appears that type equality doesn't imply the indices for the types are equal. (No `congr`

for types.)

#### Kenny Lau (Sep 20 2020 at 06:59):

I don't understand what you mean. `bool = bool`

is provable but `ff == tt`

is provably false

#### Kenny Lau (Sep 20 2020 at 06:59):

what does index mean?

#### Kyle Miller (Sep 20 2020 at 07:05):

If I have the terminology right, in `path r x y`

from above, the `x`

and `y`

are indices, and `path r x y = path r x' y'`

doesn't imply `x = x'`

or `y = y'`

. Mario gave a disproof for my simple example.

(My understanding of the issue is that there is a model of type theory where you forget all the indices.)

#### Kyle Miller (Sep 20 2020 at 07:06):

(deleted)

#### Mario Carneiro (Sep 20 2020 at 08:31):

there is a model of type theory where all types with the same cardinality are equal, and that model violates most inductive type injectivity theorems

#### Kevin Buzzard (Sep 20 2020 at 09:42):

I found crazy assertions like this very hard to understand until I realised that we could have just defined int to be a type alias for nat but with some different definition of addition and multiplication and zero and 1.

#### Kyle Miller (Sep 21 2020 at 20:06):

Another related question: If two types are equal, there's the `cast`

function which gives a bijection between their terms, and if `h : α = β`

then `heq`

seems to be something like a natural transformation from `id`

to `cast h`

, where `α`

and `β`

are regarded as categories whose objects are their terms and morphisms are equalities. Are there models where `cast h`

is a non-trivial self-bijection? For example, `cast`

from `vector α (a + (b + c))`

to `vector α ((a + b) + c)`

?

Last updated: May 14 2021 at 22:15 UTC