Much of this code is adapted from an earlier experiment. Relative to my old
experiment, I am now distinguishing "green" and "red" trees in the style of
Roslyn, where the latter instrument the former with global positioning
information via a line map. For me a "green tree" is a syntax tree, and a "red
tree" is a cursor.

I am also starting to hook up the tokenisation and parsing into the llbuild2fx
action graph.

This is as-yet untested.

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.

When instantiating the closures for record fields, we should plug in just the
appropriate prefix of the main record.