Casting Functions

Stream: new members

[Marcus Rossel]

Let's say I have (n n' : ℕ) (h : n' = n) (f : fin n → ℤ).
What's the nicest way to get f' : fin n' → ℤ from this (where ∀ x, f x = f' x)?

[Eric Wieser]

This works:

example (n n' : ℕ) (h : n' = n) (f : fin n → ℤ) : fin n' → ℤ := f ∘ fin.cast h

[Kevin Buzzard]

This is a great example of dependent type hell. It seems that in dependent type theory one has to learn to think about these questions in a certain kind of way in order to avoid pain.

[Marcus Rossel]

@Kevin Buzzard ^^ indeed. This is part of an effort to get out of dependent type hell.