In this paper, we prove that Heyting's arithmetic can be interpreted in an intuitionistic version of Russell's Simple Theory of Types without extensionality.

We show how to interpret Heyting's arithmetic in an intuitionistic version of TT, Russell's Simple Theory of Types. We also exhibit properties of finite sets in this theory and compare them with the corresponding properties in classical TT. Finally, we prove that arithmetic can be interpreted in intuitionistic TT, the subsystem of intuitionistic TT involving only three types. The definitions of intuitionistic TT and its finite sets and natural numbers are obtained in a straightforward way from the classical definitions. This (...) is very natural and seems to make intuitionistic TT an interesting intuitionistic set theory to study, beside intuitionistic ZF. (shrink)