  We introduce a new version of arithmetic in all finite types which extends
the usual versions with primitive notions of extensionality and extensional
equality. This new hybrid version allows us to formulate a strong form of
extensionality, which we call converse extensionality. Inspired by Brouwer's
notion of apartness, we show that converse extensionality can be eliminated in
a way which improves on results from our previous work. We also explain how
standard proof-theoretic interpretations, like realizability and functional
interpretations, can be extended to such hybrid systems, and how that might be
relevant to proof-mining.

Logic