Finite Sets and Natural Numbers in Intuitionistic TT Without Extensionality
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.