[Agda-dev] Implementing a solver for universe levels

[Marko Dimjašević]

Dear Agda developers,

The upcoming Agda 2.6.1 release features universe cumulativity [1]. In
an email to the Agda users mailing list (agda at lists.chalmers.se),
Jesper Cockx said the following about cumulativity [2]: "If anyone is
interested in implementing a proper solver for universe levels, please
get in touch!"

I am interested to work on this!

Would anyone be so kind to say a bit more about the problem, the
current state of universe levels and of the cumulativity feature, which
is marked experimental? Furthermore, how big an effort to implement a
solver is considered to be?

So far I made no coding contributions to Agda, though I've been a
Haskell developer.


[1] https://github.com/agda/agda/blob/release-2.6.1/CHANGELOG.md
[2] https://lists.chalmers.se/pipermail/agda/2020/011486.html


-- 
Regards,
Marko Dimjašević <marko at dimjasevic.net>
https://dimjasevic.net/marko
PGP key ID:       056E61A6F3B6C9323049DBF9565EE9641503F0AA
Learn email self-defense! https://emailselfdefense.fsf.org

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://lists.chalmers.se/pipermail/agda-dev/attachments/20200105/468f2677/attachment.sig>