Topic: equality of types
Klaus Mattis (Feb 08 2021 at 15:16):
The topic name might be slightly misleading.
Say I wanted to prove the following lemma:
lemma test (X Y : Type) (h : X = Y) (x : X) (y : Y) : x = y := sorry
The lemma is obviously false, but that is not the point.
My problem is, that I cannot even formulate the lemma, because x and y have different types, which totally makes sense.
But then I also know that the types are the same, so I should somehow be allowed to speak about equality of x and y.
Is there some way to make my example work?
Johan Commelin (Feb 08 2021 at 15:17):
Yes, this is called heterogeneous equality. You can write
x == y. But it isn't very pleasant to work with.
Kevin Buzzard (Feb 08 2021 at 22:13):
The "philosophy" is that if
X Y : Type and
a b : X then talking about
a = b is sensible, but talking about
X = Y is a bit more dangerous because
Y are "one level up" from
b, so the correct notion of "same"ness is an
e : X ≃ Y, which is defined to be maps in both directions whose composite both ways is the identity. In your example you can then talk about
e x = y, and here you avoid the dreaded
== completely. You can even see it with the
Prop universe -- it is not really reasonable to say that Fermat's Last Theorem is equal to 2+2=4, but they are logically equivalent because they're both true, and here the appropriate notion of sameness is
Eric Wieser (Feb 08 2021 at 22:22):
Except docs#propext means you really can say that
2+2=4 and Fermat's last theorem are equal.
Kevin Buzzard (Feb 08 2021 at 22:40):
The very fact that this is an axiom and some people don't believe it is already an indication that something funny is going on.
Mario Carneiro (Feb 08 2021 at 22:45):
I'm not sure that there is anyone who thinks this axiom is not true; in fact it's basically baby-HoTT, being the univalence axiom for
Mario Carneiro (Feb 08 2021 at 22:46):
If you think that types should be syntactically generated (like an inductive type) then perhaps you want to deny this axiom
Mario Carneiro (Feb 08 2021 at 22:47):
Generally speaking, something being an axiom is evidence that people think it's true, not that people think it is false
Kevin Buzzard (Feb 09 2021 at 07:24):
I think univalence is false!
Mario Carneiro (Feb 09 2021 at 07:28):
It depends on what you mean by "is" :upside_down:
Last updated: May 13 2021 at 18:26 UTC