I had an interesting idea tonight for how to a fully coherent cumulative
hierarchy of universes in an algebraic way. The idea is to have a smallness
*relation* and a shrinking operator that takes a small type and turns it into a
code.

This is algebraic, but even better, it can be interpreted into MLTT + the usual
more complicated cumulative universes with semilattice and successor. The
interpretation sends the smallness relation to the *image* of the universe
decoding map; this image exists in the algebraic sense because the decoding map
is injective.

I have added a notion of general size to factor the code appropriately. The
idea is as follows:

There is a type

Universe

that classifies small universe levels. This type is "very large", not because
of its size but because it won't be fibrant.

A "size" is either

small(U: Universe)

or it is

moderate().

For each size S, there is a type

S.codes

that classifes the S-small types.

For each code

X : S.codes

there is a type

X.decode.

--------------------------------------------

There is an inequality relation on sizes. Every small(U) is strictly lower than
moderate().

Add tests for size inequalities, fix revealed bugs