一句话：利用分离关系为逆外延性提供计算解释，并构造装配范畴模型。
本文研究强外延性形式——逆外延性（converse extensionality）的计算解释。该原理来自外延性公理的 Dialectica 解释，最早由 Howard 研究。为解释它，作者重新审视 Brouwer 的分离关系（apartness），即构造性不等式的强形式。方法上，他们给出一个范畴构造，为每个类型组合代数配备分离关系；并利用函数不仅保持相等而且还反射分离这一性质，证明由此得到的装配（assemblies）范畴模型满足逆外延性原理。这一结果为强外延性提供了计算语义，并展示了分离关系在类型论与范畴语义中的作用。
In this paper we try to find a computational interpretation for a strong form of extensionality, which we call "converse extensionality". 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 that functions reflect apartness, in addition to preserving equality, to prove that the resulting categories of assemblies model a converse extensionality principle.