[Agda-dev] Meta-theoretical implications of first class Level

[Guillaume Brunerie]

Hi Guillaume,

I've also met people who were skeptical about first-class levels in Agda,
but I personally don't really see where the problem is.
It seems pretty clear to me that there should be an interpretation of Agda
in, say, ZFC + (ω+1) inaccessible cardinals (called κ_0, ..., κ_n, …, κ_ω)
where
- "Level" is interpreted as the set of natural numbers
- "Set i" is interpreted as κ_i
- large (universe polymorphic) types like i : Level |- Set i are
interpreted as (families of) elements of κ_ω
- Pi-types take A in κ_i and B in κ_j and return something in κ_(max i j)
(works also when i or j is ω, and if j is not constant, then it gets bumped
to ω, but in those cases where max i j = ω, the Pi-type is not a term
anymore, it is simply a large type)

This allows for any kind of storing/computation/passing around of levels
and I don’t see what could go wrong with it.
But I haven’t seen any paper about this and I haven’t checked the details,
so maybe something does go wrong with it (?)

This is only an answer about consistency, I haven’t thought about more
syntactic things like decidability of type-checking, confluence, strong
normalization, and so on.

Best,
Guillaume


Den ons 19 juni 2019 09:54Guillaume Allais <guillaume.allais at ens-lyon.org>
skrev:

> Hi all,
>
> I wrote a paper for TyDe relying heavily on the fact that Levels are
> a first class notion in Agda. Following comments by reviewers, I am
> touching up the discussion on the limitations of the project and one
> of them is that other languages may be reticent to adopt such a first
> class status for Levels.
>
> Is it fair to say that the meta-theoretical consequences of being able
> to store, pass around and compute Levels are not known?
>
> Cheers,
> --
> gallais
>
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda-dev/attachments/20190619/42ca69fe/attachment.html>