Pure type systems

For a specification $\mathcal{S}=(S,\mathcal{A},\mathcal{R})$, pseudo-terms are $$M,N,A,B::=x\mid c\mid MN\mid \lambda (x:A).M\mid \prod _{x:A}B.$$ Variables $V$ and constants $C$ are disjoint, and $S\subseteq C$. The axiom set has entries $c:s$ with $s\in S$, and the product-relation entries are triples $(s_1,s_2,s_3)\in \mathcal{R}$. Compatible beta-reduction is generated by $$\frac{\phantom{X}}{(\lambda (x:A).M)N{⟶}_{\beta }M[N/x]}\mathrm{Beta}.$$ Its reflexive-transitive closure is ${⟶}_{\beta }^{\ast }$; ${=}_{\beta }$ is the equivalence relation generated by ${⟶}_{\beta }$. The complete typing sheet is

$c:s\in \mathcal{A}$

$\cdot {⊢}_{\mathcal{S}}c:s$

$\mathrm{\Gamma }{⊢}_{\mathcal{S}}A:s$$x\notin \mathrm{dom}(\mathrm{\Gamma })$

$\mathrm{\Gamma },x:A{⊢}_{\mathcal{S}}x:A$

$\mathrm{\Gamma }{⊢}_{\mathcal{S}}M:A$$\mathrm{\Gamma }{⊢}_{\mathcal{S}}B:s$$x\notin \mathrm{dom}(\mathrm{\Gamma })$

$\mathrm{\Gamma },x:B{⊢}_{\mathcal{S}}M:A$

$\mathrm{\Gamma }{⊢}_{\mathcal{S}}A:s_1$$\mathrm{\Gamma },x:A{⊢}_{\mathcal{S}}B:s_2$$(s_1,s_2,s_3)\in \mathcal{R}$

$\mathrm{\Gamma }{⊢}_{\mathcal{S}}\prod _{x:A}B:s_3$

$\mathrm{\Gamma },x:A{⊢}_{\mathcal{S}}M:B$$\mathrm{\Gamma }{⊢}_{\mathcal{S}}\prod _{x:A}B:s$

$\mathrm{\Gamma }{⊢}_{\mathcal{S}}\lambda (x:A).M:\prod _{x:A}B$

$\mathrm{\Gamma }{⊢}_{\mathcal{S}}F:\prod _{x:A}B$$\mathrm{\Gamma }{⊢}_{\mathcal{S}}N:A$

$\mathrm{\Gamma }{⊢}_{\mathcal{S}}FN:B[N/x]$

$\mathrm{\Gamma }{⊢}_{\mathcal{S}}M:A$$\mathrm{\Gamma }{⊢}_{\mathcal{S}}B:s$$A{=}_{\beta }B$

$\mathrm{\Gamma }{⊢}_{\mathcal{S}}M:B$

For the lambda cube, $S=\{\ast ,◻\}$, $\mathcal{A}=\{\ast :◻\}$, and every vertex contains $(\ast ,\ast ,\ast )$. The three independent axes add, respectively, $(◻,\ast ,\ast )$, $(◻,◻,◻)$, and $(\ast ,◻,◻)$.