Converse extensionality and apartness

TL;DR

This paper provides a categorical framework to interpret converse extensionality principles using Brouwer's apartness relation, linking constructive inequality with computational models.

Contribution

It introduces a categorical construction that endows typed combinatory algebras with an apartness relation, enabling a computational interpretation of converse extensionality.

Findings

Categories of assemblies model the converse extensionality principle

Functions reflect apartness and preserve equality in the constructed models

Provides a new link between constructive inequality and categorical semantics

Abstract

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.