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

[Jesper Cockx]

Indeed, expanding the implicit arguments you get `zero {n} : Fin (suc n)`
and `zero {suc n} : Fin (suc (suc n))`, which are definitely not
syntactically equal. There exist languages that have a notion of "equality
up to erasure" such as Cedille (https://github.com/cedille), but Agda does
not have such a notion.

-- Jesper

On Sat, Nov 7, 2020 at 3:46 PM András Kovács <puttamalac at gmail.com> wrote:

> Note `inject₁` doesn't change the syntactic form of `i`, only it's type.
>
>
> This is not correct. Inject1 changes the implicit Nat indices in Fin
> constructors. There is no notion of equality which is more "syntactic" than
> definitional equality. If two terms are not equal by refl, they are not
> syntactically equal.
>
> Matthew Daggitt <matthewdaggitt at gmail.com> ezt írta (időpont: 2020. nov.
> 7., Szo, 9:26):
>
>> 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
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201107/e231c065/attachment.html>