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 premisses-conclusion 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 well-known 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