An equality form such as makes sense
only if **A** is a type
and **a** and **b** are elements of that type.
How should we express
the idea that is well--formed?
One possibility is to use the same format as in
the case of types.
We could imagine a rule of the following form.

This rule expresses the right ideas, and it allows
well--formedness to be treated through the proof
mechanism in the same way that well--formedness is treated for types.
In fact, it is clear
that such an approach will be necessary for equality
forms if it is necessary for types because it is
essential to know that the **A** in is
well--formed.

Thus an adequate deductive apparatus is at hand for
treating the well--formedness of equalities, provided
that we treat as a type.
Does this make sense on other grounds as well?
Can we imagine an equality as denoting a type?
Or should we introduce a new category, called * Prop* for proposition,
and prove ) in Prop?
The constructive interpretation of truth of any
proposition **P** is that **P** is provable.
Thus it is perfectly sensible to regard a
proposition **P** as the type of its proofs.
For the case of an equality we make the
simplifying assumption that we are not
interested in the details of such proofs because
those details do not convey any more computational
information than is already contained in the
equality form itself.
It may be true that there are many ways to prove
, and
some of these may involve complex inductive
arguments.
However, these arguments carry
only ``equality information,'' not computational information,
so for simplicity we agree that equalities
considered as types are either empty if they
are not true or contain a single element, called
**axiom** , if they are true.

Once we agree to treat equalities as types
(and over **int**, to treat **a < b** as a type also) then a remarkable
economy in the logic is possible.
For instance, we notice that the cartesian product
of equalities, say , acts
precisely as the conjunction
.
Likewise the disjoint union, ,
acts exactly like the constructive disjunction.
Even more noteworthy is the fact that the dependent product,
say , acts exactly like the
constructive existential quantifier,
.
Less obvious, but also valid, is the interpretation
of as the universal statement,
.

We can think of the types built up
from equalities (and inequalities in the case of integer)
using , **|** and as propositions, for
the meaning of the type constructors corresponds
exactly to that of the logical operators considered
constructively. As another example of this, if **A**
and **B** are propositions then corresponds exactly
to the constructive interpretation of .
That is, proposition **A** implies proposition **B**
constructively if and only if there is a method of
building a proof of **B** from a proof of **A**,
which is the case if and only if there is a function **f**
mapping proofs of **A** to proofs of **B**.
However, given that **A** and **B** are types such an **f** exists exactly when the
type is inhabited, i.e., when there is an element of
type .

It is therefore sensible to treat propositions as types. Further discussion of this principle appears in chapters 3 and 11.

Is it sensible to consider any type, say **int** or ,
as a proposition?
Does it make sense to assert **int**?
We can present the logic and the type theory in a
uniform way if we agree to take the basic form of
assertion as ``type **A** is inhabited.''
Therefore, when we write the goal
we are asserting that given that the types in **H** are
inhabited, we can build an element of **A**.
When we want to mention the inhabiting object directly we
say that it is * extracted* from the proof, and we write
.
This means that **A** is inhabited by the object **a**.
We write the form instead of when we want
to suppress the details of how **A** is inhabited, perhaps leaving
them to be determined by a computer system as in the case of Nuprl
.

When we write we are really asserting the equality

.This equality is a type. If it is true it is inhabited by

.As another example of this interpretation, consider the goal

.This can be proved by introducing

.This is proved by introduction, and the inhabiting witness is

Thu Sep 14 08:45:18 EDT 1995