Equality of arguments from equality of structure types

Stream: lean4

[Alex Meiburg]

Any tips on how to prove this?

structure Wrap (a : Type u) where
  x : a

theorem wrap_typeInj {α β : Type u} (h : Wrap α = Wrap β) : α = β := by
  sorry

I'm having a bad time with heqs and I'm stuck here.

[Kenny Lau]

it's not provable

[Kenny Lau]

any type lemmas are basically bad

[Alex Meiburg]

This isn't provable? I'm skeptical

[Alex Meiburg]

I'm aware they're all "basically bad" but I kind of needed this.

[Kenny Lau]

I mean any inductive type is basically one more axiom, and there's absolutely nothing wrong for me to "implement" Unit and Fin 1 as two different types, but Wrap Unit and Wrap (Fin 1) as the same type

[Alex Meiburg]

In general yes, but in this case it's not clear to me that that would hold here. I mean we know that Wrap.mk / Wrap.x have to get out the 'same type as I put in'

[Alex Meiburg]

Maybe I'm not following

[Alex Meiburg]

I thought this was the kind of lemma that Wrap.noConfusion was for

[Aaron Liu]

this is not provable

[Aaron Liu]

why do you need this

[Aaron Liu]

you should never need this

[Yaël Dillies]

No indeed, this lemma is true in the cardinality model, and false in the other extremal model (whose name I forgot) some intermediate model where some same-size elements of Type u are mapped to the same element of Type u under Wrap

[Alex Meiburg]

Aaron Liu said:

why do you need this

Because I'm working in an unpleasant category with a bunch of equalities between types, and some of these type equalities would be very convenient to move back and forth across inductive types

[Aaron Liu]

the very similar looking structure Wrap' (a : Type (u + 1)) : Type u where is definitely not injective

[Aaron Liu]

maybe that makes it a bit more believable

[Alex Meiburg]

Haha, not to me, I guess my intuition was that "I have an x data inside which I can always get out"

[Aaron Liu]

haha, I tried a proof like that and there's nothing saying you can't get out data in two different ways from the same type

[Aaron Liu]

and there's nothing special about a structure projection that you can use here either, it's just another way of getting data out

[Alex Meiburg]

don't know what you mean about "two different ways", but ok
Well it's not the end of the world. This doesn't mean the main thing that I want isn't unprovable, just that I'll need to carry around a lot of extra hypotheses that α = β as I move around, where I thought that my hypotheses (x : Wrap α) ≍ (y : Wrap β) would keep it bundled together already

[Alex Meiburg]

Thanks :tear:

[Aaron Liu]

Alex Meiburg said:

Haha, not to me, I guess my intuition was that "I have an x data inside which I can always get out"

You could interpret Wrap' as having all the data, because given a Wrap' you can get data of any type you want

[Kenny Lau]

Alex Meiburg said:

I thought this was the kind of lemma that Wrap.noConfusion was for

every lemma is about terms, there is basically nothing on types

[Kenny Lau]

I think you're confused between Wrap.mk being injective and Wrap itself being injective

[Kenny Lau]

image.png

[Kenny Lau]

consider this diagram where I'm too lazy to draw out the maps (basically X, Y, Z are disjoint sets, each with three elements, represented by the three dots)

[Kenny Lau]

basically X -> Z is injective, and Y -> Z is injective

[Kenny Lau]

but on the types, both X and Y are mapped to Z

[Kenny Lau]

so {X, Y} -> {Z} is not injective

[Kenny Lau]

hope this clears your confusion

[Alex Meiburg]

That part was always no confusion of mine, but thanks :slight_smile: (pun intended)
I guess I thought this was part of Lean's type theory but it's not.