[Agda] General notion of equality for syntactically equal objects with different types from the same datatype family?

[Matthew Daggitt]

Hi everyone,
 I'm trying to prove something a lemma that looks something like:
```agda
open import Data.Fin
open import Data.Nat
open import Relation.Binary.PropositionalEquality

toℕ-inject₁ : ∀ {n} {i : Fin n} → toℕ (inject₁ i) ≡ toℕ i
toℕ-inject₁ = {!!}
```
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:
```
import Relation.Binary.HeterogeneousEquality as H using (_≅_)

toℕ-cong : ∀ {m n} {i : Fin m} {j : Fin n} → i ≅ j → toℕ i ≡ toℕ j
toℕ-cong H.refl = refl

inject₁-≅ : ∀ {n} (i : Fin n) → inject₁ i  ≅ i
inject₁-≅ zero    = H.refl
inject₁-≅ (suc i) = H.cong suc (inject₁-≅ i)
```
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.

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...
Cheers,
Matthew
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201107/53a6c744/attachment.html>