heq to eq

Stream: new members

[Kyle Miller]

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]

No it is not

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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]

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

[Kyle Miller]

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]

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

[Kyle Miller]

Isn't that type_eq_of_heq?

[Kyle Miller]

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]

I don't understand what you mean. bool = bool is provable but ff == tt is provably false

[Kenny Lau]

what does index mean?

[Kyle Miller]

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]

(deleted)

[Mario Carneiro]

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]

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]

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