Extensional equality in the classical theory of types

William W. Tait

pp. 219-234

in: Werner Depauli Schimanovich, Eckehart Köhler, Friedrich Stadler (eds), The foundational debate, Berlin, Springer, 1995

Abstract

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.