For convenience we
shall extend the relation 
to possibly open terms.
If s or t contain free variables then 
does not hold;
otherwise, it is true if and only if s has value t.
Also, define 
to mean that 
and 
.
Recall that the members of a type are its canonical members and the
terms which have those members as values. The integers
are the canonical members of
the type int. The denumerably
many atom constants are the canonical members of the type atom.
The type void is empty. The type A|B is like a disjoint
union of types A and B.
The terms inl(a) and inr(b) are canonical members so long as
and 
; a and b need not be canonical.
(The operator names inl
and inr
are mnemonic for ``inject left'' and
``inject right''.) The canonical
members of x:A#B are the terms <a,b> with 
and 
,
a and b not necessarily canonical. Note that the type from which the
second component is selected may depend on the value of the first
component.
The canonical members of the type A list represent lists of members of A.
The empty list is represented by nil. A
nonempty list with head a is
represented by a.b, where b evaluates to a member of the type A list
and represents the tail.
A term of the form t(a) is called an
application of t to a,
and a is called its argument.
The members of x:A->B are called functions,
and each
canonical member is a lambda term,
\ x.b,
whose application to any 
is a member of 
.
It is required that applications to equal members of type A
be equal.
Clearly, t(a)
if 
x:A->B and 
.
The significance of some constructors derives from the representation
of propositions as types.
A proposition represented by a type is true if and only if the type
is inhabited. The type a<b is inhabited
if and only if the value of a is less than the value of b.
The type (a=b in A) is inhabited if and only if 
.
Obviously, the type (a=a in A) is inhabited if and only if 
,
so `` a in A'' has been adopted as a notation for this type.
The members of {x:A|B} are the
members a of A such that 
is inhabited.
Types of the form {x:A|B} are called
set types.
The set constructor provides a device for specifying subtypes;
for example, {x:int|0<x} has just the positive integers
as canonical members.
The members of x,y:A//B are the members of A.
The difference between this type and A is equality.
x,y:A//B if and only if a and 
are members
of A and 
is inhabited.
Types of this form are called quotient types.
The relation 
is an equivalence relation
over A in a and 
;
this is built into the criteria for x,y:A//B being a type.
Now consider equality on the other types already discussed.
(Recall that
terms are equal in a given type if and only if they evaluate to canonical
terms equal in that type.
Recall also that 
is an equivalence relation
in a and 
when restricted to members of A.)
Members of int are equal
(in int) if and only if they have the same value.
The same goes for type atom.
Canonical members of A|B ( x:A#B, A list) are
equal if and only if they have the same outermost operator and their
corresponding immediate subterms are equal (in the corresponding types).
Members of x:A->B are equal if and only if their applications
to any member a of A are equal in 
.
We say equality on x:A->B is extensional .
The types a<b and (a=b in A) have
at most one canonical member, axiom.
Equality in {x:A|B} is just the
restriction of equality in A to {x:A|B}.
We must now consider the notion of functionality .
A term B is type --functional in 
if and only if
A is a type and 
for any a and 
such that 
.
A term b is B--functional in 
if and only if
B is type--functional in 
and 
for any a and 
such that
.
There are restrictions on type formation involving type--functionality.
These can be seen in the type formation clauses
of section 8.2 for x:A#B,
x:A->B, and {x:A|B}.
In each of these B must be type--functional in x:A.
We may now say that the members of x:A->B are the lambda terms
\x.b such that b is B--functional in 
.
In the type x,y:A//B, that B must be type--functional in both
x,y:A follows
from the fact that x:A->y:A->B->B must be a type.
There are also constraints on the typehood of x,y:A//B which
guarantee that the relation 
is an equivalence relation on members
of A and respects equality in A.
It should be noted that if A is empty then every term is type--functional
in its free variables over A. Hence, x:void#3 is a type
(with no members) even though 3 is not a type.
Equal types have the same membership and equality, but not conversely. Type equality in
is not extensional;
that is, it is not enough for type equality that two types should have
the same membership and equality. In
equal canonical types always
have the same outermost type constructor.
The relations that must hold between the
respective immediate subterms are seen easily enough in the definition of type
equality given in section 
on page .
It should be noted that in contrast to equality between types of the form
x:A#B or x:A->B,
much less is required for
{x:A|B}= {x:A|
} than type--functional
equality of B and 
in x:A. All that is required is the existence
of functions which for each 
evaluate to functions
mapping back and forth between 
and 
.
Equality between quotient types is defined similarly.
If x does not occur free in B
then A#B= x:A#B,
A->B= x:A->B,
and {A|B}= {x:A|B};
if x and y do not occur free in B then
A//B= x,y:A//B.
As a result there is no need for clauses in the type system description
giving the criteria for 
A#B and the others explicitly.
Now consider the so--called universes ,
(k positive).
The members of 
are types. The universes are
cumulative ; that is,
if j is less than k then membership and equality in 
are just
restrictions of membership and equality in 
.
Universe 
is closed
under all the type--forming operations except formation
of 
for i greater than or equal to k.
Equality (hence membership) in 
is similar to
type equality as defined previously
except that equality (membership) in 
is
required wherever type equality (typehood) was formerly required,
and although all universes are types, only those Ui such that i is less
than k are in 
. Equality in 
is the restriction
of type equality to members of 
.
So far the only noncanonical form explicitly
mentioned in
connection with the type system is application. We shall elaborate
here on a couple of forms, and it should then be easy to
see how to treat the others. The spread form is
used for computational
analysis of pairs. The pair of components is spread apart
so that the components can be used separately.
spread(e;x,y.t)
if
*
*
& T is type functional in z:( x:A#B)
*
& 
<a ,b >
*
if 
and 
Since
then for some a and b
where 
, and 
.
Hence
and
have the same value, so it is enough
that
But from our hypotheses it follows that
so it is enough that
Now
since 
x:A#B and equality respects evaluation;
therefore
in light of
T's functionality in z: (x:A#B).
The list induction form allows one to perform
inductive
analysis of lists.
list_ind(e;s;x,y.t) is a function (in e) which
halts on all members of A list. It is the function (in e) defined by primitive
recursion,
where s is the result for the base case of e= nil (in A list) and
t shows how to build the value for e= x.y (in A list) from x, y and the value
of the function being defined on y, this value being passed through u during
evaluation.
if
*
A list
*
& T is type functional in z:( A list)
*
& 
nil
*
& 
*
if 
& 
& 
Let us prove this by induction on the length of the list
represented by e, all other variables universally quantified.
Suppose 
. By definition we know that
list_ind(e;s;x,y,u.t)
and s
have the same value,
so it is enough for the base case that 
;
this is true since T is functional in 
A list,
, and 
.
Now suppose that for some a and b, a.b
, 
, and 
.
Now
and
have the same value, so it is enough that the substitution into t
is in 
.
and b represents a shorter list than e; therefore,
by inductive hypothesis
It follows that the substitution into t is in 
, so it
is enough that 
; this holds because of T's functionality
and the equality of a.b and e (in A list).
The decide form is used to discern a left from a right injection, and
to permit computation on the injected term. The ind form is used
to define functions recursively on integers.
The reader is referred to chapter 2 or to the exposition of the rules for further
elaboration of the use of noncanonical forms.