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

To do this, it was necessary to store types of globals (which we will need to
do anyway). Also, in order to forestall the "Goodbye Lenin" problem, I am
storing globals as terms rather than as values.