<div dir="ltr">Hi everyone,<br><div> I'm trying to prove something a lemma that looks something like:</div><div>```agda</div><div>open import Data.Fin</div><div>open import Data.Nat</div><div>open import Relation.Binary.PropositionalEquality</div><div><br></div><div>toℕ-inject₁ : ∀ {n} {i : Fin n} → toℕ (inject₁ i) ≡ toℕ i<br>toℕ-inject₁ = {!!}</div><div>```</div><div>Note `inject₁` doesn't change the syntactic form of `i`, only it's type. In this simple case it is easy enough to prove inductively, but I've currently got a harder case where `inject₁` is more complicated. So I was thinking about using heterogeneous equality and generalising this to something of the form:</div><div>```</div><div>import Relation.Binary.HeterogeneousEquality as H using (_≅_)<br></div><div><br></div><div>toℕ-cong : ∀ {m n} {i : Fin m} {j : Fin n} → i ≅ j → toℕ i ≡ toℕ j<br>toℕ-cong H.refl = refl<br></div><div><br></div><div>inject₁-≅ : ∀ {n} (i : Fin n) → inject₁ i  ≅ i<br></div><div>inject₁-≅ zero    = H.refl<br>inject₁-≅ (suc i) = H.cong suc (inject₁-≅ i)<br></div><div>```</div><div>The problem is of course that the two cases of `inject₁-≅` don't type check as the two sides don't have the same type. Examining the first case, we want to assert that `zero : Fin n` and `zero : Fin (suc n)` are equal. In heterogeneous equality, despite working for terms of different types, the constructor `refl` can only be applied when those two types can be proved to be propositionally equal.</div><div><br></div><div>I suspect I'm going to have to define a custom notion of equality over `Fin`, but I just thought I'd check that there isn't a more general notion of equality out there that I could use that I'm missing? It's probably a silly question, as a purely syntactic notion of equality that entirely ignores the types seems very unlikely to be undefinable. But I thought perhaps the fact that they belonged to the same datatype might give some wriggle room...</div><div>Cheers,</div><div>Matthew</div></div>