A.1 The first presentation
The objects and types of our type theory^{} may be written as terms using the following syntax, which is an extension^{} of $\lambda $calculus with variables $x,{x}^{\prime},\mathrm{\dots}$, primitive constants $c,{c}^{\prime},\mathrm{\dots}$, defined constants $f,{f}^{\prime},\mathrm{\dots}$, and term forming operations^{}
$$t::=x\mid \lambda x.t\mid t({t}^{\prime})\mid c\mid f$$ 
The notation used here means that a term $t$ is either a variable $x$, or it has the form $\lambda x.t$ where $x$ is a variable and $t$ is a term, or it has the form $t({t}^{\prime})$ where $t$ and ${t}^{\prime}$ are terms, or it is a primitive constant $c$, or it is a defined constant $f$. The syntactic markers ’$\lambda $’, ’(’, ’)’, and ’.’ are punctuation for guiding the human eye.
We use $t({t}_{1},\mathrm{\dots},{t}_{n})$ as an abbreviation for the repeated application $t({t}_{1})({t}_{2})\mathrm{\dots}({t}_{n})$. We may also use infix notation, writing ${t}_{1}\star {t}_{2}$ for $\star ({t}_{1},{t}_{2})$ when $\star $ is a primitive or defined constant.
Each defined constant has zero, one or more defining equations. There are two kinds of defined constant. An explicit defined constant $f$ has a single defining equation
$$f({x}_{1},\mathrm{\dots},{x}_{n}):\equiv t,$$ 
where $t$ does not involve $f$. For example, we might introduce the explicit defined constant $\circ $ with defining equation
$$\circ (x,y)(z):\equiv x(y(z)),$$ 
and use infix notation $x\circ y$ for $\circ (x,y)$. This of course is just composition of functions.
The second kind of defined constant is used to specify a (parameterized) mapping $f({x}_{1},\mathrm{\dots},{x}_{n},x)$, where $x$ ranges over a type whose elements are generated by zero or more primitive constants. For each such primitive constant $c$ there is a defining equation of the form
$$f({x}_{1},\mathrm{\dots},{x}_{n},c({y}_{1},\mathrm{\dots},{y}_{m})):\equiv t,$$ 
where $f$ may occur in $t$, but only in such a way that it is clear that the equations determine a totally defined function. The paradigm examples of such defined functions are the functions defined by primitive recursion on the natural numbers^{}. We may call this kind of definition of a function a total recursive definition. In computer science and logic this kind of definition of a function on a recursive data type has been called a definition by structural recursion.
Convertibility $t\downarrow {t}^{\prime}$ between terms $t$ and ${t}^{\prime}$ is the equivalence relation^{} generated by the defining equations for constants, the computation rule
$$(\lambda x.t)(u):\equiv t[u/x],$$ 
and the rules which make it a congruence^{} with respect to application and $\lambda $abstraction:

•
if $t\downarrow {t}^{\prime}$ and $s\downarrow {s}^{\prime}$ then $t(s)\downarrow {t}^{\prime}({s}^{\prime})$, and

•
if $t\downarrow {t}^{\prime}$ then $(\lambda x.t)\downarrow (\lambda x.{t}^{\prime})$.
The equality judgment $t\equiv u:A$ is then derived by the following single rule:

•
if $t:A$, $u:A$, and $t\downarrow u$, then $t\equiv u:A$.
Judgmental equality is an equivalence relation.
Title  A.1 The first presentation^{} 

\metatable 