Universes are slow

[mattam82]

Here's an idea: to check universe constraints in the checker, we first build the transitive closure of the graph, then we should get constant time comparisons. We could also use a kind of union-find like in the kernel to handle equal universe levels.