[Agda] More heterogeneous equality.

[Jesper Cockx]

Do you know of any type theory with level polymorphism that supports a rule
like that? I can agree that this would indeed be convenient in some cases,
but we should be careful of adding new unification rules whenever it seems
convenient. At least for the regular heterogeneous equality we have now, we
know that the elimination rule is equivalent with K.

For the record, my new unifier (see other thread) reports the following:

α != β of type .Agda.Primitive.Level
when checking that the pattern refl has type Set α ≅ Set β

I'm not sure if this is more or less understandable than the current error
message. At least it doesn't talk about a "heterogeneous constraint", of
which most people won't know what it means.

cheers,
Jesper

On Mon, Dec 14, 2015 at 8:58 AM, effectfully <effectfully at gmail.com> wrote:

> Hi. Agda 2.4.3 allows to define
>
>     data _≅_ {α} {A : Set α} (x : A) : ∀ {β} {B : Set β} -> B -> Set where
>       refl : x ≅ x
>
> `A' and `B' lie in different universes and the whole thing lies in
> `Set'. This is very convenient, but is it reliable? If so, can the
> definition in the standard library be replaced by this one?
>
> Agda rejects
>
>     eq : ∀ {α β} -> Set α ≅ Set β -> α ≅ β
>     eq refl = refl
>
>       -- Refuse to solve heterogeneous constraint Set α : Set (lsuc α) =?=
>       -- Set β : Set (lsuc β)
>
> Is it a natural restriction?
>
> Also, can somebody explain how Agda infers levels in data/record
> declarations now? Is there a paper?
> _______________________________________________
> 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/20151214/23cb1e1a/attachment.html