## Stream: general

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

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

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