逆外延性与分离性
Converse extensionality and apartness
AI总结：
本文为逆外延性寻找计算解释，通过范畴构造为类型化组合子代数赋予分离性关系，并利用函数反映分离性，证明组装范畴模型化逆外延性原则。
摘要：
本文试图为一种强形式的外延性寻找计算解释，我们称之为“逆外延性”。逆外延性原则作为外延性公理的Dialectica解释而出现，最早由Howard研究。为了给这些原则提供计算解释，我们重新考虑了Brouwer的分离性关系，这是一种强构造性的不等式形式。形式上，我们提供了一种范畴构造，为每个类型化组合子代数赋予分离性关系。然后，我们利用函数不仅保持相等性，还反映分离性这一性质，证明了由此产生的组装范畴模型化了逆外延性原则。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
