Lambda cube

Definition

Let $\ast$ and $\square$ be two constants, called sorts, and let $s, s_1, s_2$ range over $\set{\ast, \square}$. Terms are built from variables, the sorts, application $A\, B$, abstraction $\lambda x{:}A.\, B$ and product $\Pi x{:}A.\, B$. For a set $R \subseteq \set{\ast, \square}^2$, the system $\lambda R$ derives judgments $\Gamma \vdash A : B$ with these rules, among others.

1. Axiom: $\vdash \ast : \square$.
2. Product: for each $(s_1, s_2) \in R$, if $\Gamma \vdash A : s_1$ and $\Gamma, x{:}A \vdash B : s_2$, then $\Gamma \vdash (\Pi x{:}A.\, B) : s_2$.
3. Abstraction: if $\Gamma, x{:}A \vdash b : B$ and $\Gamma \vdash (\Pi x{:}A.\, B) : s$, then $\Gamma \vdash (\lambda x{:}A.\, b) : \Pi x{:}A.\, B$.
4. Application: if $\Gamma \vdash F : \Pi x{:}A.\, B$ and $\Gamma \vdash a : A$, then $\Gamma \vdash F\, a : B[x := a]$.
5. Conversion: if $\Gamma \vdash a : A$, $\Gamma \vdash B : s$ and $A =_\beta B$, then $\Gamma \vdash a : B$.

The remaining rules are the start, weakening and variable rules for contexts. The lambda cube consists of the eight systems $\lambda R$ with $$(\ast, \ast) \in R \subseteq \set{(\ast, \ast), (\square, \ast), (\square, \square), (\ast, \square)}.$$