[Agda] Proving equality of levels with heterogeneous equality.

[Jesper Cockx]

It's not possible to prove this in Agda because the pattern matching
unification algorithm only deals with data constructors (such as 'zero' or
'suc'), not with type constructors (such as 'Nat' or 'Set'). I don't
immediately see if your particular lemma here would break soundness, but
that doesn't say much.

-- Jesper

On Sat, Mar 9, 2019 at 9:57 PM Apostolis Xekoukoulotakis <
apostolis.xekoukoulotakis at gmail.com> wrote:

> I don't really know the theory behind this. It simply came out in practice
> because of this(1)
>
> Can anyone prove this? I think it is impossible to prove right now.
> ```
> infix 4 _≅_
>
> data _≅_ {ℓ1} {A : Set ℓ1} (x : A) : ∀ {ℓ2} → {B : Set ℓ2} → B → Set ℓ1
> where
>    refl : x ≅ x
>
> lemma : ∀{l1 l2} → {A : Set l1} → {B : Set l2}
>           → A ≅ B → l1 ≡ l2
> lemma x = {!!}
> ```
> Till now, I have considered levels as a nuance that I don't want to deal
> with.
>
> (1) : https://github.com/agda/agda-stdlib/pull/608
> _______________________________________________
> 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/20190310/bb1978a5/attachment.html>