## 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


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.)

(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