[Agda] clarification on --level-universe

[Jason Hu]

Hi all,

I know this flag move Level to its own universe. I know it disallows computing universes and I think it's the right way to do universe polymorphism. But I don't seem to find a reason why this is done in this way? What would be an issue without --level-universe? I can find a motivation for this flag anywhere.

Thanks,
Jason
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20250307/c5424119/attachment.html>