The classical theory of types in question is essentially the theory of Martin-Löf [1] but with the law of double negation elimination. I am ultimately interested in the theory of types as a framework for the foundations of mathematics and, for this purpose, we need to consider extensions of the theory obtained by adding "well-ordered types,' for example the type N of the finite ordinals; but the unextended theory will suffice to illustrate the treatment of extensional equality.