Meta-Logical Framework

This idea comes out of a discussion with Jacques Carette. The idea is essentially to have a logical framework with a sort of "internalization" operation, where you can use a theory defined within the LF as a LF itself to define more theories.

To understand this, it helps to work through exactly how a single-level LF ought to work. There, you have:

• Judgements are types.