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 term of the form ` t(a)` is called an

`\`

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

The members of ` x,y:A//B` are the members of

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` (

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

`\`

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

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 ` U i` such that

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

*

* &

* &

* if and

Since then for some

The list induction form allows one to perform
inductive
analysis of lists.
` list_ind( e;s;x,y.t)` is a function (in

if

*

* &

* &

* &

* if & &

Let us prove this by induction on the length of the list represented by

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

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.

Thu Sep 14 08:45:18 EDT 1995