Spahn rules of type theories (Rev #1)

• Bart jacobs, Categorical logic and type theory

lists the followings as the basic rules of simple type theory:

(1) identity

(2) function symbol

for $F:x_1,\dots,x_n\to x_{n+1}$ in $\Sigma$

(3) weakening

(4) contraction

(5) exchange

where we omitted the $\Gamma \vdash$ which we could prefix to every typing judgement.

From these rule one can derive a further important rule:

(6) substitution