
1.3 Equational Rules
An equation H oe M = N : t means that terms M and N are equal and of type t relative to the typing context H. An equational judgement T ` (H oe M = N : t) means that the equation is provable relative to the equational theory T 1.
Equational rules have a premissesconclusion structure much alike the typing ones and also define an inference system where a proof is sometimes called equation derivation. The categorical models the heart of the study are required to be sound w.r.t the equational rules.
2 >=?: The Simply Typed >=Calculus with Constants
and Products
Itself a variation of the simply typed >=calculus, it is the basic case on which the other two calculi under study are built. There is the wellknown CurryHoward correspondence between this calculus and the natural deduction. It can be characterised by the double slogan:
proof = term
proposition = type
2.1 Type Theory
2.1.1 Syntax
Let Tc be the set of type constants. The types are given by the syntax
t ::= c j t ! t j t ? t
where c 2 Tc. It is the set of finite terms over the signature
? = hTc; !;?i
where
8c 2 Tc:ar(c) = ; ar(!) = ar(?) = 2:
The terms are given by the syntax
M ::= c j x j >=x : t: M j MM j (M; M ) j fst(M ) j snd(M )
2.1.2 Typing Rules
i. k2dom(HC )
H ` k:HC(k)
ii. H; x:t; H0 ` x:t
1an equational theory is a set of equations