Repository | Book | Chapter
(1995) The foundational debate, Dordrecht, Springer.
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.
Publication details
DOI: 10.1007/978-94-017-3327-4_17
Full citation:
Tait, W. W. (1995)., Extensional equality in the classical theory of types, in W. Depauli Schimanovich, E. Köhler & F. Stadler (eds.), The foundational debate, Dordrecht, Springer, pp. 219-234.
This document is unfortunately not available for download at the moment.