  In this paper we try to find a computational interpretation for a strong form
of extensionality, which we call "converse extensionality". These converse
extensionality principles, which arise as the Dialectica interpretation of the
axiom of extensionality, were first studied by Howard. In order to give a
computational interpretation to these principles, we reconsider Brouwer's
apartness relation, a strong constructive form of inequality. Formally, we
provide a categorical construction to endow every typed combinatory algebra
with an apartness relation. We then exploit certain continuity principles and
that functions reflect apartness, as opposed to preserving equality, to prove
that the resulting categories of assemblies model some converse extensionality
principles.
