In Agda, universe levels are not only explicit but they are also first order. This means that you can store them in data structures and compute with them. This allows you to write generic programs in Agda's userland where you would have to resort to a meta-language in other proof assistants.

I present some of these constructions in Generic Level Polymorphic N-ary Functions.

In Agda, universe levels are not only explicit but they are also first class. This means that you can store them in data structures and compute with them. This allows you to write generic programs in Agda's userland where you would have to resort to a meta-language in other proof assistants.

I present some of these constructions in Generic Level Polymorphic N-ary Functions.