Allow defining (large) types at surface-level

[Russoul]

Currently we have only one universe. That means it's impossible to define, say, a small type of monoids at this universe.
We either have to introduce at least one more universe or a hierarchy or even more sophisticated machinery.
A much simpler and possibly not less powerful than above solution is to just introduce a large type of monoids.
We actually already have everything needed at the core-level. Just need to add syntax.