Spahn
rules of type theories
- Bart jacobs, Categorical logic and type theory
p.121-123 lists the following as the basic rules of simple type theory:
(1) identity
(2) function symbol
for in
(3) weakening
(4) contraction
(5) exchange
where we omitted (except in (4) and (5)) the which we could prefix to every typing judgement.
From these rule one can derive a further important rule:
(6) substitution