Preliminaries

There are a couple things about the λΠ-calculus and related systems before this is started.

Terms, Types, and Kinds

λΠ, like many other formal systems, has a three tiered system. These involve three syntatic classes, terms (expressions), types (sorts) and kinds. In a language like Agda, there is not a very clear distinction between these three. In a system like Agda’s, every kind is a type, and every type is an expression.

Here, we work in a much more statified system. Namely, these three classes are entierly distinct in a signature. That is, nothing is more than one of a term, type, or kind. Of these, kinds describe types, which in turn describe terms.