# Zulip Chat Archive

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