eng
episciences.org
Logical Methods in Computer Science
1860-5974
2022-12-20
Volume 18, Issue 4
10.46298/lmcs-18(4:13)2022
7306
journal article
Converse extensionality and apartness
Benno van den Berg
Robert Passmann
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.
https://lmcs.episciences.org/7306/pdf
Mathematics - Logic
Computer Science - Logic in Computer Science
Mathematics - Category Theory