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

[Guillaume Allais]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda-dev/attachments/20190619/274ef919/attachment.sig>