Basics

The first part of any language we must define is its syntax.

Syntax

The most important layer of the syntax is that of terms

Caution

Often the terms of λΠ are further subdived into canonical terms (those that are in normal form) and atomic terms (those that are always in normal form). For simplicities sake, we use the syntax for each, as ultimately the typing rules are suffeciently strict to ensure that the terms are used correctly.

Here, we call the syntax of the terms $\phi$:

$$\phi ::= x | A | \lambda_x \sigma_0 . \phi_0 | (\phi_0 \phi_1) \\ \sigma ::= S | \Pi_x \sigma_0 . \sigma_1 | \Lambda_x \sigma_0 . \sigma_1 | (\sigma_0 \phi_0) \\ \kappa ::= \Pi_x \sigma_0 . \kappa_0 | \ast$$

Terms

The terms, in more detail, describe the proofs of judgements. In addition, they also describe the syntax of the object logic.

1. Variables: a variable is a term bound in the context, $\Gamma$. Ultimately, the techinical details are not important (in the end we end up using De Brujn indices).
2. Constants: a constant is a term bound free in the signature. It must be bound to a valid $\sigma$,