Zulip Chat Archive

Stream: general

Topic: equality of types


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

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

view this post on Zulip 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 X and Y are "one level up" from a and b, so the correct notion of "same"ness is an equiv, 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 .

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Feb 09 2021 at 07:24):

I think univalence is false!

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