[Agda] clarification on --level-universe

[Naïm Favier]

You can always read the discussions on the issue tracker: https://github.com/agda/agda/issues/6272

On 07/03/2025 03:30, Jason Hu wrote:
> 	
> You don't often get email from fdhzs2010 at hotmail.com. Learn why this is important <https://aka.ms/LearnAboutSenderIdentification>
> 	
> 
> 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
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda