[Agda] Proving equality of levels with heterogeneous equality.

[Jason -Zhong Sheng- Hu]

I don't think so, though. Level should just be a counter for the universes, so it doesn't have to be big.

open import Level
Foo : Set
Foo = Level

This code actually works in Agda.

Sincerely Yours,

Jason Hu
________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of Stefan Monnier <monnier at iro.umontreal.ca>
Sent: March 10, 2019 2:18 PM
To: agda at lists.chalmers.se
Subject: Re: [Agda] Proving equality of levels with heterogeneous equality.

> 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.

I'm not surprised it's not possible, but I'm surprised by
this explanation.  I'd have thought the first reason is that

    ℓ₁ ≡ ℓ₂

is ill-typed because

    ℓ₁, ℓ₂ : Level
    (≡) : {ℓ : Level} → {A : Set ℓ} → A → A → Set ℓ

and there is no ℓ for which `Level : Set ℓ`


        Stefan

_______________________________________________
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/59767a02/attachment.html>