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 that functions reflect apartness, in addition to preserving equality, to prove that the resulting categories of assemblies model a converse extensionality principle.
翻译:在这份文件中,我们试图找到一种对强烈扩展形式的计算解释,我们称之为“反扩展性 ” 。这些反扩展性原则是作为扩展性轴的对等解释产生的,首先由霍华德研究。为了对这些原则进行计算解释,我们重新考虑布鲁韦尔的分离关系,这是一种强烈的建设性不平等形式。形式上,我们提供了一种明确的构造,将每一个打字的交错代数与分离关系归结在一起。然后,我们利用这些功能反映分裂,除了维护平等外,还利用这些功能来证明由此形成的集会类别是反向延伸原则。