So far we have talked exclusively about types and their
members.
We now want to talk about simple declarative statements.
In the case of the integers many interesting facts
can be expressed as equations between terms.
For example, we can say that a number n is even by
writing 
.
In Nuprl
the equality relation on int is built--in;
we write 
.
In fact, each type A comes with an equality relation
written 
.
The idea that types come equipped with an equality
relation is very explicit in the writings of
Bishop [Bishop 67].
For example, in The Foundation of Constructive Analysis,
he says,
``A set is defined by describing what must be
done to construct an element of the set, and what must be
done to show that two elements of the set are equal.''
The notion that types come with an equality is central
to Martin-Löf
's type theories as well.
The equality relations 
play a dual role in
Nuprl
in that they can be used to express type membership relations
as well as equality relations within a type.
Since each type comes with such a relation, and since
is a sensible relation only if a and b are
members of A, it is possible to express the idea that a
belongs to A by saying that 
is true.
In fact, in Nuprl
the form 
is really shorthand for
.
The equality statement 
has the curious property
that it is either true or nonsense.
If a has type A then 
is true; otherwise, 
is not a sensible statement because 
is sensible only if
a and b belong to A.
Another way to organize type theory is to use a
separate form of judgement to say that a is in
a type, that is, to regard 
as distinct from
.
That is the approach taken by Martin-Löf
.
It is also possible to organize type theory without
built--in equalities at all except for the most
primitive kind.
We only need equality on some two--element type,
say a type of booleans, 
;
we could then define equality on int as a function from
int into 
The fact that each type comes equipped with equality
complicates an understanding of the rules,
as we see when we look at functions.
If we define a function 
then
we expect that if 
then
.
This is a key property of functions, that they respect
equality.
In order to guarantee this property there are a host of rules of the form that if part of an expression is replaced by an equal part then the results are equal. For example, the following are rules.
