How to cast types properly

Stream: new members

[Jihoon Hyun]

#mwe

def α : Type _ := sorry

def β : Type _ := α

def func : α → α := sorry

instance : HasEquiv β := sorry

example (b : β) : (func b : β) ≈ b := by
  sorry

I want to make the example work as expected. Of course it is possible to define an explicit coersion method, like of\alpha : \alpha \to \beta, but it will lead to not-simp-normal-form error if the theorem of\alpha a = a is simp, which is very reasonable if I'm right.

[Kevin Buzzard]

func b is defeq abuse so I'm not sure what "work as expected" means here, if you commit defeq abuse then it's hard to know what to expect.

[Jihoon Hyun]

So I'd like to state an equivalence between func b and b as an element of type \beta. In my case, \alpha is actually a list, so it bothers me quite a lot.

[Kevin Buzzard]

But func is not a function on beta

[Jihoon Hyun]

Then should I make a copy of func and its related theorems which works with \beta?

[Kevin Buzzard]

And of\alpha a = a is also defeq abuse so shouldn't be a simp lemma or indeed a lemma

[Kevin Buzzard]

Jihoon Hyun said:

Then should I make a copy of func and its related theorems which works with \beta?

Sure! In mathlib we have plenty of examples of avoiding defeq abuse by carefully using of\alpha and to\alpha even on types which are defeq

[Edward van de Meent]

usually in this kind of situation, we have a few casting equivalences (for example, docs#FreeMonoid.toList) which allow you to convert from one to the other

[Edward van de Meent]

see for example docs#FreeMonoid.countP'

[Jihoon Hyun]

Edward van de Meent said:

see for example docs#FreeMonoid.countP'

Thank you for a nice example!