Fix levels of universes

[mmontin]

We need to gain some genericity in the newest versions of our work. There are two options:

• either go back to setw, but that's questionable whether or not that's even possible
• or just use and additional level parameters spread throughout the library

[pedagand]

Concerning the first point, my worry is that we will have to compose the functors in Set\omega with Applicative functors, which may not happily live in Set\omega.

Concretely: one should start from #2, reintroduce Set\omega and see whether that can be fixed or understand what is broken.

[pedagand]

@mmontin would you mind taking over this one?