equality of types

Stream: general

[Klaus Mattis]

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]

Yes, this is called heterogeneous equality. You can write x == y. But it isn't very pleasant to work with.

[Kevin Buzzard]

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]

Except docs#propext means you really can say that 2+2=4 and Fermat's last theorem are equal.

[Kevin Buzzard]

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]

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]

If you think that types should be syntactically generated (like an inductive type) then perhaps you want to deny this axiom

[Mario Carneiro]

Generally speaking, something being an axiom is evidence that people think it's true, not that people think it is false

[Kevin Buzzard]

I think univalence is false!

[Mario Carneiro]

It depends on what you mean by "is" :upside_down: