Zulip Chat Archive

Stream: new members

Topic: heq to eq


view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 20 2020 at 03:24):

No it is not

view this post on Zulip 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 }

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Sep 20 2020 at 04:29):

Why would you want to compare nil entries on different basepoints?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 20 2020 at 04:34):

Note that <x, x, nil> = <y, y, nil> -> x = y is provable

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Sep 20 2020 at 06:48):

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

view this post on Zulip Kyle Miller (Sep 20 2020 at 06:51):

Isn't that type_eq_of_heq?

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip Kenny Lau (Sep 20 2020 at 06:59):

what does index mean?

view this post on Zulip 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.)

view this post on Zulip Kyle Miller (Sep 20 2020 at 07:06):

(deleted)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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