# Type Prediction Systems

Sarthak Dash
IBM Research AI
Yorktown Heights, NY
<EMAIL_ADDRESS>
&Nandana Mihindukulasooriya
IBM Research AI
Yorktown Heights, NY
<EMAIL_ADDRESS>
&Alfio Gliozzo
IBM Research AI
Yorktown Heights, NY
<EMAIL_ADDRESS>
&Mustafa Canim
IBM Research AI
Yorktown Heights, NY
<EMAIL_ADDRESS>
###### Abstract

Inferring semantic types for entity mentions within text documents is an
important asset for many downstream NLP tasks, such as Semantic Role
Labelling, Entity Disambiguation, Knowledge Base Question Answering, etc.
Prior works have mostly focused on supervised solutions that generally operate
on relatively small-to-medium-sized type systems. In this work, we describe
two systems aimed at predicting type information for the following two tasks,
namely  a) A TypeSuggest module, an _unsupervised_ system designed to predict
types for a set of user-entered query terms, and  b) An Answer Type prediction
module, that provides a solution for the task of determining the correct type
of the answer expected to a given query.  Our systems generalize to arbitrary
type systems of _any_ sizes, thereby making it a highly appealing solution to
extract type information at any granularity.

##  1 Introduction

Knowledge graphs are generally defined as “a graph of data intended to
accumulate and convey knowledge of the real world, whose nodes represent
entities of interest and whose edges represent relations between these
entities" [5]. Knowledge graphs are designed as directed edge-labelled graphs
(also known as multi-relational graphs) where each edge has a direction and a
relation type. Most of them use Semantic Web technologies such as RDF(S) and
OWL for representing these knowledge graphs with explicit semantics. RDF type
or “is-a" relation of relation is one very important relation type that
defines the type of each node. For example, if the node is “New York", it
could be typed as a “city" or “populated city".

Identifying these types can provide vital information in many knowledge graph
related tasks such as Knowledge Base Question Answering (KBQA) [4], Table
Understanding [12], Table Question Answering (Table QA), etc. For e.g. when a
question is asked by the user corresponding to a KBQA or a Table QA task, it
is crucial to understand the type of the correct answer pertaining to the
question before proceeding to answer search.

In this paper, we introduce two systems for predicting type information,
namely  a) The TypeSuggest module, an _unsupervised_ system designed to
predict types for a set of user entered seed query terms, and  b) The Answer
Type prediction module, that _pulls-in_ types from the Semantic Web in a
distantly supervised fashion, to predict the type of the correct answer for
the user provided question.  The input to the TypeSuggest module is a list of
seed query terms, and the output returned by the module is a ranked list of
types from some predefined type system. The Answer Type Prediction module
takes in question string as input, and returns a ranked list of types for the
correct answer. Both of these systems _do not_ require manual annotations,
thereby making them highly appealing to be used as it is, in a wide-variety of
domains.

##  2 Related Work

There have been many studies over the years focusing on this problem. In this
work, we limit the discussion to those that go beyond predicting a fixed set
of _coarse-grained_ answer types.

One of the early works [7] involved using fine-grained and coarse-grained
types together in a hierarchical classifier, albeit the types were _not_
overlapping. Other works such as [6, 8] use hand-crafted features or features
obtained from pre-existing grammars in conjunction with machine learning
models (such as SVMs, Logistic Regression, etc.) to build answer type
prediction models. Furthermore, [2] uses additional manual annotations to
perform fine-grained typing of entity mentions within a sentence. More
recently, SeMantic AnsweR Type prediction task (SMART) [9] was proposed as an
ISWC 2020 Semantic Web challenge in which eight answer type systems
participated. The top system at SMART 2020 formulates the type prediction task
as an extreme multi-label text classification (XMC) problem and uses
X-Transformers [1] for type prediction.

In comparison, our proposed method utilizes _types_ from the Semantic Web in a
distantly-supervised fashion, thereby requiring no manual annotations. In our
approach, one can also determine the granularity level of the final _types_ ,
since these are obtained from open domain ontologies.

##  3 Type Suggestion Module

In this section, we introduce the TypeSuggest module designed to generate
types for a set of seed query terms input by the user. It is also a _pre-
requisite_ needed to build the Answer Type Prediction module. In essence,
given a set of seed terms as input, TypeSuggest provides a ranked list of
_relevant types_ as output. Implementation wise, it uses a predefined type
system $\mathcal{TS}$ such as DBPedia, Wikidata, or Yago as a source of
potential _possible_ types.

Given a list of seed query terms, $\mathcal{Q}=\\{\emph{Amazon, Sony,
IBM}\\}$, in order to figure out relevant _types_ , TypeSuggest employs the
following steps:

### Entity Linking:

The first step links the terms in $\mathcal{Q}$ to a taxonomy in
$\mathcal{TS}$. This is done by first normalizing the string and then checking
similarity with the entity labels in $\mathcal{TS}$. Once complete, we get a
list $\mathcal{L}_{\mathcal{S}}$ of seed terms that are linked to their
corresponding entity within $\mathcal{TS}$. The query terms that can not be
linked are ignored.

### Seed Expansion:

The second step is to expand the seed terms $\mathcal{L}_{\mathcal{S}}$, if
necessary. The minimum number of seed terms required to facilitate next step
is denoted by $k$ (typically set by user). Given the seed terms
$\mathcal{L}_{\mathcal{S}}$, an expansion step (performed only if
$|\mathcal{L}_{\mathcal{S}}|<k$) uses a pretrained Word2Vec [10] model (with
vocab $\mathcal{V}$) to augment $\mathcal{L}_{\mathcal{S}}$ in the following
way: For each $x\in\mathcal{L}_{\mathcal{S}}$, it identifies the most similar
term $y\in\mathcal{V}\setminus\mathcal{L}_{\mathcal{S}}$ which links to a
valid entity in $\mathcal{TS}$. This term $y$ gets added to
$\mathcal{L}_{\mathcal{S}}$, and the process is repeated until
$|\mathcal{L}_{\mathcal{S}}|=k$.

### Type Identification:

The final step is to identify the types based on the linked seed terms. For
each linked seed term, we look for its _type_ (denoted by the function Type)
within the taxonomy $\mathcal{TS}$, thus yielding a _type-vocabulary_
$\mathcal{TV}$. For each _type_ $t^{\prime}\in\mathcal{TV}$, we define,

$\textsc{Count}(t^{\prime})=|\\{x\in\textsc{SeedExpansion}(\mathcal{L}_{\mathcal{S}})|\textsc{Type}(x)=t^{\prime}\\}|$

Furthermore, for each $t^{\prime}\in\mathcal{TV}$, we define
EntityCount($t^{\prime})$ as the number of entities associated with the _type_
$t^{\prime}$ in $\mathcal{TS}$. Moreover, let $Z(t^{\prime})$ denote the total
number of entities of type $t^{\prime}$ present in $\mathcal{TS}$.

We rank the _types_ in $\mathcal{TV}$ using the following tf-idf like
function,

$\forall
t^{\prime}\in\mathcal{TV},\quad\textsc{Score}(t^{\prime})=\textsc{Count}(t^{\prime})\times[\log
Z(t^{\prime})-\log\textsc{EntityCount}(t^{\prime})]$

and return the ranked list as the output of the TypeSuggest module.

##  4 Answer Type Prediction

In this section, we use the TypeSuggest module described in the previous
section to build our proposed Answer Type Prediction model.

As input, our model takes a list of question-answer pairs, i.e.
$\zeta=(q_{i},a_{i}),1\leq i\leq N$ from a large external general-purpose QA
dataset. This list of question-answer pairs $\zeta$ goes through the following
pre-processing steps.

### Type Acquisition:

For each question-answer pair $(q_{i},a_{i})$, we define the _type_ of the
answer $a_{i}$ as follows,

$\textsc{Type}(a_{i})=\left\\{\begin{array}[]{ll}[(\textsc{NER}(a_{i}),\textsc{Score})]&\quad\mbox{if
}\textsc{NER}(a_{i})\in\mathcal{N}\\\
\textsc{TypeSuggest}(a_{i})&\quad\mbox{elsewhere}\end{array}\right.$ (1)

where $\mathcal{N}=\texttt{\\{Date, Cardinal, Ordinal, Quantity, Money,
Percent\\}}$ is a set of coarse named entity types, NER denotes an off-the-
shelf Named Entity Recognition System and Score is a fixed numerical value,
i.e. a _hyper-parameter_ of our proposed model.

Using this criterion, we obtain a ranked list of _types_ $T_{i}$ for each
question-answer pair $(q_{i},a_{i})$, and construct our augmented dataset,
$\zeta^{\textsc{Aug}}=(q_{i},a_{i},T_{i})$. Note that $\forall i,1\leq i\leq
N,T_{i}$ denotes a ranked list of _types_.

### Type Restriction:

The augmented dataset $\zeta^{\textsc{Aug}}$ built in the previous step is
highly likely to yield a large number of unique _types_ because the predefined
type systems $\mathcal{TS}$ are usually very large in size. In this step, we
restrict ourselves to top $k$ (by frequency) unique types and drop the rest.
Here, $k$ is a hyper-parameter of our model.

Out of the _types_ that remain, we keep only those whose frequency is less
than a pre-set threshold count $c$, thus ensuring that the _generic_ types
such as yago:Thing, yago:Abstraction etc. are removed, which allows the
_learner_ (to be described later) not to be _biased_ towards these generic
types.

Let $\mathcal{T}$ denote the union of the left-over _types_ with the set
$\mathcal{N}$ defined above. This set constitutes our _Type Vocabulary_ ,i.e.
we build a model (described below) which given a question $q$ as input,
returns a ranked list of entries from $\mathcal{T}$ as output.

This _frequency_ based pruning step transforms the augmented dataset
$\zeta^{\textsc{Aug}}$ in the following fashion. For each entry
$(q_{i},a_{i},T_{i})\in\zeta^{\textsc{Aug}}$, wherein
$T_{i}=(t^{j}_{i},s^{j}_{i}),\text{}1\leq j\leq|T_{i}|$ denotes the ranked
list of types corresponding to answer $a_{i}$, we have the following update,

$\tilde{t}^{j}_{i}=\left\\{\begin{array}[]{ll}t^{j}_{i}&\quad\mbox{if
}t^{j}_{i}\in\mathcal{T}\\\
\operatorname*{arg\,min}_{x^{*}\in\mathcal{T}}\textsc{Dist}(x,x^{*})&\quad\mbox{if
}t^{j}_{i}\notin\mathcal{T}\end{array}\right.$ (2)

wherein Dist between two types $x$ and $x^{*}$ is defined as the length of the
shortest path between types $x$ and $x^{*}$ within the type system
$\mathcal{TS}$ encoded as a graph.

Thus, this step outputs a pre-processed dataset
$\zeta^{\textsc{Aug}}_{\textsc{Restr}}=(q_{i},a_{i},\tilde{T}_{i})$, wherein
each instance now contains an updated list of _types_
$\tilde{T}_{i}=(\tilde{t}^{j}_{i},s^{j}_{i}),\text{}1\leq
j\leq|\tilde{T}_{i}|$ for answer string $a_{i}$ according to Equation 2.

This pre-processed dataset $\zeta^{\textsc{Aug}}_{\textsc{Restr}}$ forms the
training dataset for our proposed _neural network_ architecture for the
_Answer Type Prediction_ task, which is described in detail in the next
section.

### Neural Network Architecture:

We next describe the detailed architecture of our proposed _Answer Type
Prediction_ model. As shown in Figure 1, it consists of three steps:

  * •

Preparing _Type Embeddings_ from the Type vocabulary $\mathcal{T}$.

  * •

Encoding input _question_ $q_{i}$ to its corresponding question embedding
$\vec{q}_{i}$.

  * •

Building a simple learning framework that uses $\vec{q}_{i}$ and $\mathcal{T}$
as inputs, and produces a list of ranked _types_ $T^{\textsc{Pred}}_{i}$ as
output.

The predicted list of _types_ $T^{\textsc{Pred}}_{i}$ is compared with
$\tilde{T}_{i}$ (from $\zeta^{\textsc{Aug}}_{\textsc{Restr}}$) in order to
calculate _Weighted Cross Entropy_ loss values, which is minimized during
training procedure. We now describe each of these _three_ sections in detail.

Figure 1: Architecture of _Answer Type Prediction_ model

### Preparing Type Embeddings:

We use a pre-trained Glove model [11], and encode each entry within the Type
vocabulary $\mathcal{T}$ to initialize a Type Embedding matrix $S$. Let us
illustrate via an example.

  * •

If the type within $\mathcal{T}$ is dbo:person or Wikidata:person, we assign
it the Glove vector for “person”.

  * •

If the type is yago:WikicatAmericanPeople, this type gets assigned the vector
$0.5*[v(\texttt{american})+v(\texttt{people})]$, where $v(\texttt{american})$
and $v(\texttt{people})$ denote the Glove embeddings for the terms “american”
and “people” respectively.

We split WikicatAmericanPeople to Wikicat, American, and People using regular
expressions. The term Wikicat is ignored.

  * •

If the type is yago:Person100007846, this type gets assigned the Glove vector
for “Person”. The numerical part (extracted via _regex_) is ignored.

  * •

Any _term_ not present in Glove gets initialized randomly.

### Preparing Question Embedding:

As illustrated in Figure 1, given a training instance
$(q_{i},a_{i},\tilde{T}_{i})\in\zeta^{\textsc{Aug}}_{\textsc{Restr}}$, the
question string is tokenized and encoded via a _bi-directional_ LSTM [3]. The
vectors from both the unidirectional LSTMs are concatenated together to yield
a matrix $Q_{i}$ of dimensions $|q_{i}|\times 2D$, where $|q_{i}|$ denotes the
number of tokens in the question string $q_{i}$ and $D$ is the size of the
vectors output by the unidirectional LSTMs.

The _Aggregation_ layer then consists of the following steps,

  * •

Calculate $\psi_{i}=Q_{i}\cdot\textsc{ATT}$ where matrix ATT is of dimensions
$2D\times 1$, and $\cdot$ represents matrix multiplication.

  * •

Normalize $\psi_{i}$ to have unit $l_{2}$ norm, and calculate
$Q_{i}\otimes\psi_{i}$, where $\otimes$ denotes element-wise multiplication.

  * •

Calculate $\vec{q}_{i}=\sum_{j=1}^{|q_{i}|}(Q_{i}\otimes\psi_{i})_{[j,:]}$,
i.e. sum together all the rows in the matrix obtained in the previous step.

  * •

Here, ATT denotes the model _parameters_ learned during training.

Using these steps, the question string $q_{i}$ is mapped to its _vector_
representation $\vec{q}_{i}$. Next, we describe how $\vec{q}_{i}$ interacts
with the Type Embedding matrix $S$.

### Putting it Together:

In this step, our model performs a _matrix-vector_ multiplication
$\vec{q}^{T}_{i}S$, followed by a sampled softmax operation, in order to
obtain a predicted list $\mathcal{P}_{i}$ of _scores_ , one per type. Using
this predicted list $\mathcal{P}_{i}$ and the known list of types
$\tilde{T}_{i}$, the loss function (also referred to as _Weighted Cross
Entropy_ loss) is calculated as,

$\mathcal{J}_{i}=-\sum_{(\tilde{t}^{j}_{i},s^{j}_{i})\in\tilde{T}_{i}}s^{j}_{i}\log\mathcal{P}^{\tilde{t}^{j}_{i}}_{i}$

where $\mathcal{P}^{\tilde{t}^{j}_{i}}_{i}$ corresponds to the _system
predicted_ score for the type $\tilde{t}^{j}_{i}$.

During inference time, given a query question $q_{\textsc{Query}}$, we use the
learned model parameters to build the query embedding
$\vec{q}_{\textsc{Query}}$ as well as the embedding matrix $S$. Finally, we
perform a matrix-vector multiplication, i.e. $\vec{q}^{T}_{\textsc{Query}}S$
to obtain a ranked list of _predicted_ scores, which is shown to the user.

##  5 Conclusion

In this paper, we introduced two systems for predicting type information,
namely  a) The TypeSuggest module, an _unsupervised_ system designed to
predict types for a set of user entered seed query terms, and  b) The Answer
Type prediction module, that _pulls-in_ types from the Semantic Web in a
distantly supervised fashion, to predict the type of the correct answer for
the user provided question.  We described both of these systems in detail,
starting with the data ingestion phase, followed by the pre-processing phase
and ended up with a neural network based learner for the Answer Type
prediction module. Furthermore, we demonstrated that both these systems _do
not_ require manual annotations, thereby making them highly appealing to be
used as it is, in a wide-variety of domains.

## References

  * [1] Chang, W.-C., Yu, H.-F., Zhong, K., Yang, Y., and Dhillon, I. S. Taming pretrained transformers for extreme multi-label text classification.  In Proceedings of the 26th ACM SIGKDD International Conference on Knowledge Discovery & Data Mining (2020), pp. 3163–3171.
  * [2] Choi, E., Levy, O., Choi, Y., and Zettlemoyer, L. Ultra-fine entity typing.  In Proceedings of the 56th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers) (Melbourne, Australia, July 2018), Association for Computational Linguistics, pp. 87–96.
  * [3] Hochreiter, S., and Schmidhuber, J. Long short-term memory.  Neural computation 9, 8 (1997), 1735–1780.
  * [4] Höffner, K., Walter, S., Marx, E., Usbeck, R., Lehmann, J., and Ngonga Ngomo, A.-C. Survey on challenges of question answering in the semantic web.  Semantic Web 8, 6 (2017), 895–920.
  * [5] Hogan, A., Blomqvist, E., Cochez, M., d’Amato, C., de Melo, G., Gutierrez, C., Gayo, J. E. L., Kirrane, S., Neumaier, S., Polleres, A., et al. Knowledge graphs.  arXiv preprint arXiv:2003.02320 (2020).
  * [6] Khoury, R. Question type classification using a part-of-speech hierarchy.  In Autonomous and Intelligent Systems (Berlin, Heidelberg, 2011), M. Kamel, F. Karray, W. Gueaieb, and A. Khamis, Eds., Springer Berlin Heidelberg, pp. 212–221.
  * [7] Li, X., and Roth, D. Learning question classifiers.  In Proceedings of the 19th International Conference on Computational Linguistics - Volume 1 (USA, 2002), COLING ’02, Association for Computational Linguistics, p. 1–7.
  * [8] Lopez, V., Fernández, M., Motta, E., and Stieler, N. Poweraqua: Supporting users in querying and exploring the semantic web.  Semant. Web 3, 3 (Aug. 2012), 249–265.
  * [9] Mihindukulasooriya, N., Dubey, M., Gliozzo, A., Lehmann, J., Ngomo, A.-C. N., and Usbeck, R. SeMantic AnsweR Type prediction task (SMART) at ISWC 2020 Semantic Web Challenge.  CoRR/arXiv abs/2012.00555 (2020).
  * [10] Mikolov, T., Sutskever, I., Chen, K., Corrado, G., and Dean, J. Distributed representations of words and phrases and their compositionality, 2013.
  * [11] Pennington, J., Socher, R., and Manning, C. GloVe: Global vectors for word representation.  In Proceedings of the 2014 Conference on Empirical Methods in Natural Language Processing (EMNLP) (Doha, Qatar, Oct. 2014), Association for Computational Linguistics, pp. 1532–1543.
  * [12] Zhang, S., and Balog, K. Web table extraction, retrieval, and augmentation: A survey.  ACM Transactions on Intelligent Systems and Technology (TIST) 11, 2 (2020), 1–35.


# Converse extensionality and apartness

Benno van den Berg<EMAIL_ADDRESS>and  Robert Passmann
<EMAIL_ADDRESS>Institute for Logic, Language and Computation, Universiteit
van Amsterdam, Postbus 90242, 1090 GE Amsterdam, The Netherlands

(Date: 22 October, 2021)

###### Abstract.

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.

The research of the second author was supported by a doctoral scholarship of
the _Studienstiftung des deutschen Volkes_.

##  1\. Introduction

Following Kreisel one of the main concerns of proof theory has become the
extraction of hidden computational information from proofs. For this purpose
Gödel’s Dialectica interpretation (combined with negative translation, if
necessary) has proven itself to be indispensable. Indeed, within proof mining
functional interpretations of various kinds have become a sophisticated and
flexible tool for extracting additional qualitative and quantitative
information from proofs (see [2]).

One of the hardest principles to interpret using a functional interpretation
is the principle of function extensionality. This principle, which says that
two functions are equal if they yield the same output on the same input, is
pervasive in mathematics. But it has proven difficult to interpret using the
Dialectica interpretation, the reason being that the Dialectica interpretation
requires one to interpret a stronger form of extensionality, which we have
dubbed _converse extensionality_ :

$\mathsf{CE}_{n}:\quad\exists X\,\forall\Phi^{n+2}\,\forall f,g\,\big{(}\,\Phi
f\not=_{0}\Phi g\to f(X\Phi fg)\neq_{0}g(X\Phi fg)\,\big{)}.$

Note that this is equivalent to

$\exists X\,\forall\Phi^{n+2}\,\forall f,g\,\big{(}\,f(X\Phi fg)=_{0}g(X\Phi
fg)\to\Phi f=_{0}\Phi g\,\big{)}$

since equality of type 0 is decidable. As shown by Howard (see [8, Appendix]),
$\mathsf{CE}_{0}$ cannot be witnessed in the term model of Gödel’s $T$ and
$\mathsf{CE}_{1}$ is unprovable in Zermelo-Fraenkel set theory (without
choice). This has often been taken as an indication that a computational
interpretation of function extensionality is well-nigh impossible.

The starting point for this paper was the question whether the situation is
really that hopeless. Our idea is that by a suitable enrichment of data it
might still be possible to interpret (fragments of) converse extensionality.
For this we are looking at Brouwer’s notion of _apartness_.

Brouwer’s idea was that equality might not be a primitive concept and could be
defined as the negation of a strong notion of inequality called apartness. The
paradigmatic example are the real numbers, where two reals $r$ and $s$ are
apart when there are disjoint intervals with rational endpoints $I_{1}$ and
$I_{2}$ such that $r\in I_{1}$ and $s\in I_{2}$. Equality of real numbers can
then be defined as not being apart. The notion of apartness has continued to
play a role in constructive mathematics to this very day (see [1] for a recent
example).

Typical properties of the apartness relation $\mathrel{\\#}$ are the
following:

$\begin{array}[]{c}\lnot x\mathrel{\\#}x\\\ x\mathrel{\\#}y\Rightarrow
y\mathrel{\\#}x\\\ x\mathrel{\\#}y\Rightarrow(z\mathrel{\\#}x\lor
z\mathrel{\\#}y)\end{array}$

We will refer to these properties as _reflexivity_ , _symmetry_ and
_transitivity_ , because these axioms ensure that equality $x=y:=\lnot
x\mathrel{\\#}y$ has said properties.

Our first step is the observation (see also [9]) that on all the finite types
equality can indeed be defined as the negation of a suitable notion of
apartness. But that means that one may require functionals $f$ of type
$\sigma\to\tau$ to come equipped with additional data that explains how from
evidence that $fx$ and $fy$ are apart one obtains evidence that $x$ and $y$
are apart. Our initial results do indeed suggest that by enriching functionals
with this data one may interpret certain forms of converse extensionality,
although the results are not (yet) as strong as we had hoped.

To formulate the results that we have obtained so far, we use the notion of a
typed combinatory algebra (tca), basically a model of Gödel’s $T$. We show
that from every tca (including the term model of Gödel’s $T$) one can define a
new tca, which we have dubbed the _apartness types_. Our main result is that
by using modified realizability over these apartness types one can interpret
$\mathsf{CE}_{0}$. This shows (_pace_ Howard) that it might still be possible
to interpret $\mathsf{CE}_{0}$ using terms from Gödel’s $T$. To interpret
stronger principles ($\mathsf{CE}_{1}$ and higher) we currently have to use
tcas which satisfy suitable continuity principles.

For proving our results, we have decided to formulate them in a categorical
framework, using categories of assemblies. So in Section 2 of the paper we
will recall the definition of the category of assemblies over a tca, following
Longley [5]. We will also discuss the internal logic of the assemblies over a
tca there: as far as we are aware, these results have not appeared earlier in
the literature, but will not surprise the experts. In Section 3 we will show
that the assemblies over what we will call an extensional tca satisfy
principles reminiscent of Kreisel’s modified realizability. These results were
first obtained by Mees de Vries [10] for one specific extensional tca: here we
show that they hold more generally for any extensional tca. Finally, in
Section 4 we introduce the apartness types and show that in the category of
assemblies over the apartness types the converse extensionality principle
$\mathsf{CE}_{0}$ holds. We have also included an appendix which explains our
results from a proof-theoretic perspective.

Finally, we note that all our results are constructively valid, unless
explicitly noted otherwise.

##  2\. The logic of assemblies

The purpose of this section is to recall the definition of a typed combinatory
algebra (tca) and the category of assemblies over a typed combinatory algebra.
These definitions are due to Longley [5] and can also be found in [4] and [6].
We deviate from these sources by making two small changes: first of all, we
will only consider total combinatory algebras, because all the examples that
we will be interested in in this paper are total. Secondly, we include in the
type structure of a typed combinatory algebra both finite sum types and a unit
type. Our reason for doing so are is that this allows us to prove that the
assemblies over a tca form a Heyting category, which will be the main result
of this section.

###  2.1. Typed Combinatory Algebras

We will start by defining typed combinatory algebras, the total variant of the
typed partial combinatory algebras as in [5].

######  Definition 2.1.

A _typed combinatory algebra_ (tca) consists of a set $\mathcal{T}$ of types
with the following data:

  1. (i)

binary operations $\times$, $\rightarrow$, $+$ on $\mathcal{T}$, and
distinguished types $\bot,\top,N$,

  2. (ii)

a set $|T|$ of realizers for every $T\in\mathcal{T}$,

  3. (iii)

a total application function $\cdot_{S,T}:|S\rightarrow T|\times|S|\to|T|$,

such that for all $U,S,T\in\mathcal{T}$ there are elements

$\displaystyle\mathsf{exf}\in|\bot\to S|,\quad\mathsf{t}\in|\top|,$
$\displaystyle\mathsf{k}_{S,T}\in|S\to T\to
S|,\quad\mathsf{s}_{S,T,U}\in|(S\to T\to U)\to(S\to T)\to(S\to U)|,$
$\displaystyle\mathsf{pair}_{S,T}\in|S\to T\to S\times
T|,\quad\mathsf{fst}_{S,T}\in|S\times T\to
S|,\quad\mathsf{snd}_{S,T}\in|S\times T\to T|,$
$\displaystyle\mathsf{inl}_{S,T}\in|S\to S+T|,\quad\mathsf{inr}_{S,T}\in|T\to
S+T|,$ $\displaystyle\mathsf{case}_{S,T,U}\in|(S\to U)\to(T\to U)\to(S+T\to
U)|,$ $\displaystyle\mathsf{0}\in|N|,\quad\mathsf{succ}\in|N\to
N|,\quad\mathsf{R}_{S}\in|S\to(N\to(S\to S))\to(N\to S))|,$

satisfying the following conditions

$\displaystyle\mathsf{k}\,a\,b=a,\quad\mathsf{s}\,a\,b\,c=a\,c\,(b\,c),$
$\displaystyle\mathsf{fst}\,(\mathsf{pair}\,a\,b)=a,\quad\mathsf{snd}\,(\mathsf{pair}\,a\,b)=b,$
$\displaystyle\mathsf{case}\,a\,b\,(\mathsf{inl}\,x)=a\,x,\quad\mathsf{case}\,a\,b\,(\mathsf{inr}\,x)=b\,x,$
$\displaystyle\mathsf{R}\,a\,b\,\mathsf{0}=a,\quad\mathsf{R}\,a\,b\,(\mathsf{succ}\,n)=b\,n\,(\mathsf{R}\,a\,b\,n),$

for $a$, $b$, $c$, $x$ and $n$ of the corresponding types.

######  Remark 2.2.

As is customary in the theory of combinatory algebras, we usually omit the
application $\cdot$ and write $a\,b$ or $a(b)$ instead of $a\cdot b$. In fact,
we already started to do so when formulating the equations that the
combinators should satisfy in the previous definition. In addition, the
convention is that $\cdot$ associates to the left, so that $a\,b\,c\,d$ has to
be read as $((a\cdot b)\cdot c)\cdot d$. Moreover, in any tca a form of lambda
abstraction is available, in a manner similar to ordinary combinatory algebras
(for which, see [7]).

######  Definition 2.3.

If $\mathcal{T}$ is a tca, we will refer to the smallest set of types in
$\mathcal{T}$ containing $\top$ and $N$ and closed under $\to$ and $\times$ as
the _finite types_ in $\mathcal{T}$. In addition, we will also use natural
numbers to refer to specific finite types, with $0:=N$ and $n+1:=n\to N$.

######  Definition 2.4.

A typed combinatory algebra will be called

  1. (i)

_consistent_ if $\mathsf{0}\not=\mathsf{succ\,0}$.

  2. (ii)

_standard_ if the mapping $\mathbb{N}\to|N|$ obtaining by sending $n$ to the
numeral $\overline{n}=\mathsf{succ}^{n}\mathsf{0}$ is a bijection.

  3. (iii)

_extensional_ if for all types $S$ and $T$ the mappings

$\displaystyle|S\times T|\to|S|\times|T|$
$\displaystyle:x\mapsto(\mathsf{fst}\,x,\mathsf{snd}\,x)$ $\displaystyle|T\to
S|\to|S|^{|T|}$ $\displaystyle:x\mapsto\lambda y.x\cdot y$

are injective, and $\mathsf{t}$ is the sole element of $|\top|$.

######  Remark 2.5.

Note that the map $p:|S|\times|T|\to|S\times
T|:(x,y)\mapsto\mathsf{pair}\,x\,y$ is always injective, as it is a section of
$x\mapsto(\mathsf{fst}\,x,\mathsf{snd}\,x)$. For this reason we will often use
$(x,y)$ as an abbrevation for $\mathsf{pair}\,x\,y$. Hence, if $\mathcal{T}$
is extensional, the map $p$ will actually be a bijection (but this will not be
the case in general).

As in the case of partial combinatory algebras, every tca admits some
recursion theory, see, e.g., van Oosten’s book [7, Chapter 1]. In particular,
for every fixed $n\in\mathbb{N}$, we can code finite sequences
$(x_{0},x_{1},\dots,x_{n})$ of length $n$, and $i$-th projections
$\mathsf{proj}_{i}$ using just $\mathsf{pair}$, $\mathsf{fst}$ and
$\mathsf{snd}$.

######  Example 2.6.

Examples of typed combinatory algebras are abundant.

  1. (i)

Every partial combinatory algebra $\mathcal{A}$ gives rise to a tca by taking
the powerset of $\mathcal{A}$ as the set of types, with $|X|=X$, and the
operations appropriately defined. We can also restrict to those subsets of
$\mathcal{A}$ that are inhabited: this also gives one a tca.

  2. (ii)

We consider Kleene’s first algebra $\mathcal{K}_{1}$ as a tca in the sense of
(i) of the previous example.

  3. (iii)

Similarly, $\mathcal{K}_{2}^{\mathrm{rec}}$ is the tca obtained as the
recursive submodel of Kleene’s second algebra $\mathcal{K}_{2}$.

  4. (iv)

The closed terms of Gödel’s $T$ form a tca, provided we take a version of
Gödel’s $T$ which includes finite sum and unit types. The types are the types
of Gödel’s $T$ and the realizers of a type consist of the closed terms of that
type. This shows that unbounded search is generally not available in tcas.

  5. (v)

If $\mathcal{C}$ is a cartesian closed category with a natural numbers object
and finite sums, we can regard $\mathcal{C}$ as a tca as follows: the types
will be the objects in $\mathcal{C}$, while $|X|={\rm Hom}_{\mathcal{C}}(1,X)$
for any object $X$ in $\mathcal{C}$. In fact, this example would still work if
we assumed that all the structure in $\mathcal{C}$ is _weak_ (by that we mean
that we weaken the universal property by only requiring existence of a certain
arrow; we drop the requirement that that arrow is also unique). But if
$\mathcal{C}$ is genuinely cartesian closed and also _well-pointed_ (in that
two parallel arrows $f,g:X\to Y$ will be equal whenever $fh=gh$ for any arrow
$h:1\to X$), then the resulting tca will be extensional.

######  Lemma 2.7.

Every tca $\mathcal{T}$ contains an element $d\in|N\to N\to N|$ such that for
all $a,b\in\mathbb{N}$ we have that

$d\overline{a}\overline{b}=\begin{cases}\overline{0},&\text{ if }a\neq b,\\\
\overline{1}&\text{ if }a=b.\end{cases}$

###### Proof.

It is easy to check that $d:=\mathsf{R}_{0\to
0}(\mathsf{R}_{0}(\mathsf{succ}\,\mathsf{0})\mathsf{k}_{0,0})(\lambda
xy.\mathsf{R}_{0}\mathsf{0}y)$ works. ∎

######  Proposition 2.8.

Let $\mathcal{T}$ be a consistent tca. Then the following hold:

  1. (i)

The map $\mathbb{N}\to|N|:n\mapsto\overline{n}$ is injective.

  2. (ii)

The maps $|A|\to|A+B|:a\mapsto\mathsf{inl}\,a$ and
$|B|\to|A+B|:b\mapsto\mathsf{inr}\,b$ have disjoint images.

###### Proof.

(i) follows from the previous lemma. For (ii), consider

$h:=\mathsf{case}(\lambda x.\overline{0})(\lambda x.\overline{1})\in|A+B\to
N|$

and note that $h(\mathsf{inl}\,a)=\overline{0}$ while
$h(\mathsf{inr}\,b)=\overline{1}$. ∎

###  2.2. Assemblies

Following Longley [5], we generalise the usual category of assemblies over a
pca, and define a category of assemblies on a tca $\mathcal{T}$.

######  Definition 2.9.

Let $\mathcal{T}$ be a tca. An _assembly_ on $\mathcal{T}$ is a triple
$(X,A,\alpha)$, where $X$ is a set, $A$ a type of $\mathcal{T}$, and
$\alpha:X\to\operatorname{Pow}^{*}(|A|)$ (where $\operatorname{Pow}^{*}(|A|)$
being the collection of inhabited subsets of $|A|$). A morphism of assemblies
$f:(X,A,\alpha)\to(Y,B,\beta)$ is a function $f:X\to Y$ such that there exists
an element $e\in|A\to B|$ with the property that whenever $a\in\alpha(x)$,
then $ea\in\beta(f(x))$. We say that $e$ _tracks_ $f$, and refer to
$(X,A,\alpha)$ with $X$.

We denote the resulting category by $\mathbf{Asm}_{\mathcal{T}}$. We might
omit any mention of the tca $\mathcal{T}$ whenever it is clear from the
context or irrelevant which specific tca we are referring to.

Our immediate goal is now to show that $\mathbf{Asm}_{\mathcal{T}}$ is a
cartesian closed category with a natural numbers object and finite disjoint
coproducts. We will content ourselves with describing all the relevant
constructions, leaving a verification of their correctness to the reader. To
this end, let $(X,A,\alpha)$ and $(Y,B,\beta)$ be assemblies.

Initial Object:

The initial object is $(\emptyset,\bot,\emptyset)$.

Terminal Object:

The terminal object is $(\left\\{0\right\\},\top,\varphi)$, where $\varphi$ is
the map $0\mapsto\left\\{\mathsf{t}\right\\}$.

Product:

The product of $X$ and $Y$ is $(X\times Y,A\times B,\chi)$, where $\chi$ is
the map
$(x,y)\mapsto\left\\{k\,:\,\mathsf{fst}\,k\in\alpha(x),\mathsf{snd}\,k\in\beta(y)\right\\}$.

Pullback:

Given morphisms $f:(X,A,\alpha)\to(Z,C,\gamma)$ and
$g:(Y,B,\beta)\to(Z,C,\gamma)$, their pullback is $(P,A\times
B,\chi\upharpoonright P)$, where

$P=\left\\{(x,y)\in X\times Y\,:\,f(x)=g(y)\right\\},$

$\chi$ is as before and the maps $P\to X$ and $P\to Y$ are the projections.

Coproduct:

The coproduct of $X$ and $Y$ is $(X+Y,A+B,\gamma)$, where $\gamma$ is the map
defined by
$\mathsf{inl}(x)\mapsto\left\\{\mathsf{inl}\,z\,:\,z\in\alpha(x)\right\\}$ and
$\mathsf{inr}(y)\mapsto\left\\{\mathsf{inr}\,z\,:\,z\in\beta(y)\right\\}$.
Note that finite coproducts are stable under pullback.

Equaliser:

Let $f,g:(X,A,\alpha)\to(Y,B,\beta)$. The equaliser of $f$ and $g$ is
$(E,A,\alpha\upharpoonright E)$ where $E=\left\\{x\in
X\,:\,f(x)=g(x)\right\\}$ and $e:E\to X$ is the inclusion.

Natural Numbers Object:

Consider $(\mathbb{N},N,\nu)$, where $\nu$ is the map
$n\mapsto\left\\{\bar{n}\right\\}$. The map $z:1\to\mathbb{N}$ is given by
$0\mapsto 0$ and witnessed by $\lambda x.\mathsf{0}\in|\top\to N|$. The map
$s:\mathbb{N}\to\mathbb{N}$ is defined by $n\mapsto n+1$ and witnessed by
$\mathsf{succ}$.

Exponential:

We have that $X^{Y}=(Z,B\to A,\gamma)$, where $Z$ is the set of morphisms
$Y\to X$ and $\gamma(f)$ is the set of elements tracking $f$.

######  Theorem 2.10.

The category $\mathbf{Asm}_{\mathcal{T}}$ of assemblies is a cartesian closed
category with a natural numbers object and finite disjoint coproducts. ∎

###  2.3. A hyperdoctrine

Our next goal is to show that $\mathbf{Asm}_{\mathcal{T}}$ is a Heyting
category. To that purpose a simplified presentation of the subobject
hyperdoctrine of $\mathbf{Asm}_{\mathcal{T}}$ will prove useful.

######  Definition 2.11.

Let $(X,A,\alpha)$ be an assembly. A _predicate on $(X,A,\alpha)$_ is a tuple
$(B,\beta)$ consisting of a type $B$ and a map $\beta:X\to\mathcal{P}(|B|)$
for which there is an element $f\in|B\to A|$ such that $b\in\beta(x)$ implies
$f\cdot b\in\alpha(x)$.

We say that a predicate $(B,\beta)$ is a _subpredicate_ of $(C,\gamma)$ and
write $(B,\beta)\leq(C,\gamma)$ if there is an element $f\in|B\to C|$ such
that for all $x\in X$, if $b\in\beta(x)$, then $f\cdot b\in\gamma(x)$. Note
that this defines a _preorder of predicates on $(X,A,\alpha)$_.

######  Proposition 2.12.

The preorder of subobjects of $(X,A,\alpha)$ as a thin category and the
category of predicates of $(X,A,\alpha)$ are equivalent.

###### Proof.

Given a predicate $({B},\beta)$ on some assembly $(X,A,\alpha)$ as witnessed
by $f_{B}\in|B\to A|$, we can define an assembly $(Y_{B},{B},\beta),$ where
$Y_{B}=\left\\{x\in X\,:\,\beta(x)\neq\emptyset\right\\}$. Note that
$(Y_{B},B,\beta)$ is a subobject of $(X,A,\alpha)$, witnessed by $f_{B}$. If
$({B},\beta)\leq({C},\gamma)$ witnessed by some $f$, then the inclusion
$Y_{B}\subseteq{Y}_{C}$ is witnessed by $f$, i.e., ${Y}_{B}\subseteq{Y}_{C}$
as subobjects of $(X,A,\alpha)$.

Conversely, if $(Y,B,\beta)$ is a subobject of $(X,A,\alpha)$, i.e., there is
a monomorphism $f:(Y,B,\beta)\to(X,A,\alpha)$, then we can obtain a predicate
$(C_{Y},\gamma_{Y})$ on $(X,A,\alpha)$, where $C_{Y}=B$ and
$\gamma_{Y}(x)=\bigcup_{y\in f^{-1}(x)}\beta(y)$ for $x\in X$. If
$(Y,B,\beta)\subseteq(Z,D,\delta)$ as subobjects of $(X,A,\alpha)$, then there
is an element $f\in|C\to D|$ witnessing this fact. By our definitions, this
morphism also witnesses that $(C_{Y},\gamma_{Y})\leq(C_{Z},\gamma_{Z})$.

In fact, we just defined functors ${Y}_{(-)}$ and $B_{(-)}$ between the thin
categories $\operatorname{Sub}(X,A,\alpha)$ of subobjects of $(X,A,\alpha)$
and predicates of $(X,A,\alpha)$. A routine check shows that
$B_{{Y}_{(B,\beta)}}=(B,\beta)$ and ${Y}_{B_{(Y,B,\beta)}}\cong{Y}$. We can
thus conclude that both functors are full, faithful and essentially
surjective, i.e., an equivalence of categories. ∎

Let us start by noting that the predicates on $(X,A,\alpha)$ form a pre-
Heyting algebra. From the previous proposition it then follows that
$\operatorname{Sub}(X,A,\alpha)$ is a pre-Heyting algebra as well.

Top Element:

The top element of $P(X,A,\alpha)$ is $(A,\alpha)$.

Bottom Element:

The bottom element of $P(X,A,\alpha)$ is $(\bot,\emptyset)$.

Conjunction:

We have that $(B,\beta)\wedge(C,\gamma)=(B\times C,\beta\times\gamma)$.

Disjunction:

$(B,\beta)\wedge(C,\gamma)=(B+C,\delta)$ with
$\delta(x)=\\{\mathsf{inl}\,y\,:\,y\in\beta(x)\\}\cup\\{\mathsf{inr}\,y\,:\,y\in\gamma(x)\\}$.

Implication:

$(C,\gamma)\Rightarrow(B,\beta)=(A\times(C\to B),\delta)$, where
$x\in\delta(x)$ whenever $\mathsf{fst}\,x\in\alpha(x)$ and
$\mathsf{snd}\,x\in|C\to{B}|$ such that if $n\in\gamma(x)$, then
$(\mathsf{snd}\,x)\,n\in\beta(x)$.

We are now ready to define a hyperdoctrine
$P:\mathbf{Asm}_{\mathcal{T}}^{\mathrm{op}}\to\mathbf{preHA}$ (where
$\mathbf{preHA}$ is the category of pre-Heyting algebras) such that
$P(X,A,\alpha)$ is the collection of all predicates on $(X,A,\alpha)$.

If $f:(Y,B,\beta)\to(X,A,\alpha)$ is a morphism of apartness assemblies, then
we define $Pf:P(X,A,\alpha)\to P(Y,B,\beta)$ by stipulating that:

$(Pf)(C,\gamma)=(C\times B,\gamma_{f}),$

where for $y\in Y$ we define that:

$\gamma_{f}(y)=\gamma(f(y))\times\beta(y):=\\{\,\mathsf{pair}\,m\,n\,:\,m\in\gamma(f(y)),n\in\beta(y)\,\\}$

Note that $(Pf)(C,\gamma)=B_{f^{*}Y_{(C,\gamma)}}$.

We define $\exists_{f}:P(Y,B,\beta)\to P(X,A,\alpha)$ by

$\exists_{f}(C,\gamma)=(C,\gamma_{\exists}),$

where

$\gamma_{\exists}(x)=\bigcup_{y\in f^{-1}(x)}\gamma(y).$

######  Proposition 2.13.

The morphism $\exists_{f}$ is the left adjoint of $P(f)$.

###### Proof.

As we are working with thin categories, it suffices to show that the following
equivalence holds:

$\exists_{f}(C,\gamma)\leq_{P(X,A,\alpha)}(D,\delta)\iff(C,\gamma)\leq_{P(Y,B,\beta)}(Pf)(D,\delta)$

for $(C,\gamma)\in P(X,A,\alpha)$ and $(D,\delta)\in P(Y,B,\beta)$.

For the first direction, assume that $\exists_{f}(C,\gamma)\leq(D,\delta)$.
This means that there is an element $g\in|C\to D|$ such that
$n\in\gamma_{\exists}(x)$ implies that $g\cdot n\in\delta(x)$. To show that
$(C,\gamma)\leq(Pf)(D,\delta)$ it suffices to provide an element $h\in|C\to
D\times B|$ such that $m\in\gamma(y)$ implies $hm\in\delta_{f}(y)$. Let
$e_{C}\in|C\to B|$ be a witness for $(C,\gamma)\in P(Y,B,\beta)$, and take
$h:=\lambda m.\mathsf{pair}(gm)(e_{C}m)$. It follows that if $m\in\gamma(y)$,
then $hm\in\delta(f(y))\times\beta(y)=\beta_{f}(y)$.

For the other direction, assume that $(C,\gamma)\leq(Pf)(D,\delta)$, i.e.,
there is an element $h\in|C\to D\times B|$ such that if $n\in\gamma(y)$, then
$hn\in\delta(f(y))\times\beta(y)$. Now, if $n\in\gamma_{\exists}(x)$, then
there is some $y\in f^{-1}(x)$ such that $n\in\gamma(y)$. Hence,
$\mathsf{fst}\,(h\,n)\in\delta(f(y))=\delta(x)$. This shows that $g:=\lambda
n.\mathsf{fst}\,(h\,n)$ witnesses that $\exists_{f}(C,\gamma)\leq(D,\delta)$.
∎

The map $\forall_{f}:P(Y,B,\beta)\to P(X,A,\alpha)$ is defined by
$\forall_{f}(D,\delta)=(A\times(B\to D),\delta_{\forall})$, where
$x\in\delta_{\forall}(x)$ if and only if $\mathsf{fst}\,x\in\alpha(x)$ and
$\mathsf{snd}\,x\in|B\to D|$ has the property that
$(\mathsf{snd}\,x)\,k\in\delta(y)$ for all $k\in\beta(y)$ and $y\in
f^{-1}(x)$.

######  Proposition 2.14.

The morphism $\forall_{f}$ is the right adjoint of $P(f)$.

###### Proof.

It suffices to show that the following equivalence holds:

$(C,\gamma)\leq_{P(X,A,\alpha)}\forall_{f}(D,\delta)\iff(Pf)(C,\gamma)\leq_{P(Y,B,\beta)}(D,\delta)$

for $(C,\gamma)\in P(X)$ and $(D,\delta)\in P(Y)$.

For the first direction, suppose that
$(C,\gamma)\leq_{P(X,A,\alpha)}\forall_{f}(D,\delta)$ is witnessed by
$g\in|C\to A\times(B\to D)|$ such that if $n\in\gamma(x)$, then
$gn\in\delta_{\forall}(x)$. Let $h:=\lambda
m.(\mathsf{snd}\,g(\mathsf{fst}\,m))(\mathsf{snd}\,m)$. If
$m\in\gamma_{f}(y)$, then $\mathsf{fst}\,m\in\gamma(f(y))$ and
$\mathsf{snd}\,m\in\beta(y)$. Hence,
$g(\mathsf{fst}\,m)\in\delta_{\forall}(f(y))$ such that
$hm=(\mathsf{snd}\,(g(\mathsf{fst}\,m)))(\mathsf{snd}\,m)\in\delta(y)$.

For the second direction, assume that $(Pf)(C,\gamma)\leq(D,\delta)$. This
means that there is an element $g\in|C\times B\to D|$ such that if
$k\in\gamma_{f}(y)$, then $gk\in\delta(y)$. We show that $h:=\lambda
k.\mathsf{pair}\,(e_{C}k)\,(\lambda l.g(\mathsf{pair}\,k\,l))$ witnesses that
$(C,\gamma)\leq\forall_{f}(D,\delta)$: Let $k\in\gamma(x)$. As $(C,\gamma)\in
P(X,A,\alpha)$, let $e_{C}\in|C\to B|$ be a witness for $(C,\gamma)\in
P(Y,B,\beta)$. It follows that $e_{C}k\in\alpha(x)$. Furthermore, let
$l\in\beta(y)$ for some $y\in f^{-1}(x)$. Then
$\mathsf{pair}\,k\,l\in\gamma(f(y))\times\alpha(x)=\gamma_{f}(y)$, and hence,
$g(\mathsf{pair}\,k\,l)\in\delta(y)$. These calculations show that
$hk\in\delta_{\forall}(x)$. ∎

######  Proposition 2.15.

The morphisms $P(f)$, $\exists_{f}$ and $\forall_{f}$ satisfy the Beck-
Chevalley condition, i.e., if

${X}$${Y}$${Z}$${W}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{h}$$\scriptstyle{k}$

is a pullback square in $\mathbf{Asm}$, then the squares

${P(X)}$${P(Y)}$${P(Z)}$${P(W)}$$\scriptstyle{\exists_{f}}$$\scriptstyle{P(g)}$$\scriptstyle{\exists_{k}}$$\scriptstyle{P(h)}$

and
${P(X)}$${P(Y)}$${P(Z)}$${P(W)}$$\scriptstyle{\forall_{f}}$$\scriptstyle{P(g)}$$\scriptstyle{\forall_{k}}$$\scriptstyle{P(h)}$

both commute.

###### Proof.

We leave the verification that the left hand square commutes to the reader;
from this the commutativity of the right hand square follows by adjointness. ∎

######  Theorem 2.16.

The category $\mathbf{Asm}_{\mathcal{T}}$ of assemblies is a Heyting category.
∎

We conclude this section with a lemma which will prove useful later:

######  Lemma 2.17.

Suppose $(C,\gamma)$ is a predicate on an assembly $(X,A,\alpha)$. If $|\bot|$
is inhabited, then we can we put $\lnot(C,\gamma)=(A,\beta)$ with
$\beta(x)=\bigcup\\{\alpha(x)\,:\,\gamma(x)=\emptyset\\}$.

###### Proof.

Suppose $\mathsf{f}\in|\bot|$. Note that according to definition above
$(C,\gamma)\to(\bot,\emptyset)=(A\times(C\to\bot),\delta)$ with
$x\in\delta(x)$ whenever $\mathsf{fst}\,x\in\alpha(x)$,
$\mathsf{snd}\,x\in|C\to\bot|$ and $\gamma(x)$ is empty. This means that
$(C,\gamma)\to(\bot,\emptyset)\leq(A,\delta)$ is witnessed by
$\mathsf{f}\in|A\times(C\to\bot)\to A|$, while
$(A,\delta)\leq(C,\gamma)\to(\bot,\emptyset)$ is witnessed by $\lambda
x.\mathsf{pair}\,x\,(\lambda y.\mathsf{f})\in|A\to(A\times(C\to\bot))|$. ∎

######  Remark 2.18.

The assumption that $|\bot|$ is inhabited may sound paradoxical. However,
there are many examples of tcas which satisfy this assumption: for instance,
the collection of inhabited subsets of a pca $\mathcal{A}$. Indeed, tcas for
which $|\bot|$ is inhabited play an important role in this paper: the reason
is that we are interested in forms of modified realizability. The idea behind
the category-theoretic treatment of modified realizability is that there is a
distinction between the actual and potential realizers of a statement, where
every statement, including $\bot$, has a potential realizer; of course, $\bot$
does not have an actual realizer (see [7]). In the categories of assemblies
that the we will discuss below the elements of $|\bot|$ are the _potential_
realizers of $\bot$.

##  3\. Assemblies for modified realizability

In this section we will take a closer look at the category of assemblies
$\mathbf{Asm}_{\mathcal{T}}$ over an _extensional_ tca $\mathcal{T}$. For some
interesting examples of extensional tcas, we refer to [5, 4, 6] as well as the
next section. We will show that in that case we can regard $\mathcal{T}$ as a
category which embeds into $\mathbf{Asm}_{\mathcal{T}}$. In addition, in the
internal logic of $\mathbf{Asm}_{\mathcal{T}}$ the characteristic principles
of modified realizability hold: the axiom of choice for finite types as well
as the independence of premise principle if $|\bot|$ is inhabited. This
generalises the contents of Chapter 2 in the MSc thesis by Mees de Vries [10]
supervised by the first author.

_Throughout this section $\mathcal{T}$ will be an extensional tca._

###  3.1. Embedding types into assemblies

From any extensional $\mathcal{T}$ we can construct a category which we will
also denote by $\mathcal{T}$. The objects of this category are the types of
$\mathcal{T}$ and its morphisms $A\to B$ are the elements of $|A\to B|$; we
will also refer to these morphisms as _morphisms of types_. The identity arrow
is given by $\lambda x.x$ and the composition of $f$ and $g$ by $\lambda
x.g(f(x))$; the axioms for a category follow from the extensionality of the
tca $\mathcal{T}$. In fact, using extensionality one can show that
$\mathcal{T}$ is a well-pointed and cartesian closed category, with products
given by $A\times B$ and exponentials by $A\to B$. For that reason, we may
also write $B^{A}$ instead of $A\to B$.

In addition, there is a functor

$E:\mathcal{T}\to\mathbf{Asm}_{\mathcal{T}}$

which sends a type $A$ to $E(A)=(|A|,A,\alpha)$ with $\alpha(x)=\\{x\\}$,
while $(Ef)(x)=f(x)$. This functor $E$ is clearly full and faithful. We now
take a closer look at its image.

######  Definition 3.1.

An assembly $(X,A,\alpha)$ is called _modest_ if, for all $x,y\in X$, if
$a\in\alpha(x)$ and $b\in\alpha(y)$ are such that $a=b$, then $x=y$. We say
that $(X,A,\alpha)$ is _strongly modest_ if, additionally, for all $x\in X$
and $a,b\in\alpha(x)$ we have that $a=b$. We say that an assembly
$(X,A,\alpha)$ is _exhaustive_ if for all $a\in|A|$, there is $x\in X$ such
that $a\in\alpha(x)$. Finally, we say that an assembly is a _base_ or _basic_
if it is both exhaustive and strongly modest.

######  Theorem 3.2.

The functor $E:\mathcal{T}\to\mathbf{Asm}_{\mathcal{T}}$ is full and faithful.
Moreover, all the assemblies in the image of this functor are basic and every
basic assembly is isomorphic to an assembly in the image of this functor.

###### Proof.

Note that by definition $E(A)$ is a base, and a straightforward calculation
shows that $EA\cong(X,A,\alpha)$ for any basic assembly $(X,A,\alpha)$. ∎

In fact, more is true: the functor $E$ preserves the cartesian closed
structure. To show this, we need the following lemma.

######  Lemma 3.3 (Lifting of Morphisms).

Let $(X,A,\alpha)$ be a strongly modest assembly and $(Y,B,\beta)$ be a modest
exhaustive assembly. If $f:A\to B$ is a morphism of types, then there is a
unique morphism $\bar{f}:(X,A,\alpha)\to(Y,B,\beta)$ of assemblies tracked by
$f$.

###### Proof.

We construct $\bar{f}$ as follows. Given $x\in X$, let $\bar{f}(x)\in Y$ be
the unique element such that $f(a)\in\beta(\bar{f}(x))$ for all
$a\in\alpha(x)$. The map $\bar{f}$ is well-defined because $(X,A,\alpha)$ is
strongly modest and $(Y,B,\beta)$ is both modest and exhaustive. By
construction $\bar{f}$ is witnessed by $f$ and hence, $\bar{f}$ is a morphism
of assemblies.

For the uniqueness, let $\bar{f}^{\prime}:X\to Y$ be a morphism of assemblies
witnessed by $f$. Let $x\in X$ and $a\in\alpha(x)$. Then
$f(a)\in\beta(\bar{f}^{\prime}(x))$ and $f(a)\in\beta(\bar{f}(x))$. By modesty
of $Y$, it follows that $\bar{f}^{\prime}(x)=\bar{f}(x)$. ∎

######  Proposition 3.4.

In $\mathbf{Asm}_{\mathcal{T}}$ the assemblies which are modest are closed
under finite products and exponentials, as are the basic assemblies. Moreover,
$E$ preserves the cartesian closed structure.

###### Proof.

First of all, let us note that $E(\top)$ is a terminal object in
$\mathbf{Asm}_{\mathcal{T}}$ because $\mathsf{t}$ is the sole element of
$|\top|$.

Second, let $(X,A,\alpha)$ and $(Y,B,\beta)$ be two modest assemblies and
consider their product $(X\times Y,A\times B,\alpha\times\beta)$. If
$\bigcup\mathrm{Im}(\alpha)=|A|$ and $\bigcup\mathrm{Im}(\beta)=|B|$, it
follows that $\bigcup\mathrm{Im}(\alpha\times\beta)=|A|\times|B|$, i.e.
$X\times Y$ is exhaustive.

For modesty, let $(x_{0},y_{0}),(x_{1},y_{1})\in X\times Y$ and
$(a_{0},b_{0})\in(\alpha\times\beta)(x_{0},y_{0})$ and
$(a_{1},b_{1})\in(\alpha\times\beta)(x_{1},y_{1})$ such that
$(a_{0},b_{0})=(a_{1},b_{1})$. This means that $a_{0}=a_{1}$ and $b_{0}=b_{1}$
such that $a_{i}\in\alpha(x_{i})$ and $b_{i}\in\beta(y_{i})$. So if $X$ and
$Y$ are modest, it follows that $x_{0}=x_{1}$ and $y_{0}=y_{1}$. Hence
$X\times Y$ is modest as well.

For strong modesty, let $(x,y)\in X\times Y$ such that
$(a_{0},b_{0})\in(\alpha\times\beta)(x,y)$ and
$(a_{1},b_{1})\in(\alpha\times\beta)(x,y)$. By our assumption that $X$ and $Y$
are strongly modest, it follows that $a_{0}=a_{1}$, $b_{0}=b_{1}$, and hence
that $(a_{0},b_{0})=(a_{1},b_{1})$.

Third, we consider exponentials. Again, let $(X,A,\alpha_{A})$ and
$(Y,B,\alpha_{B})$ be two modest assemblies and let $(C,B\to A,\gamma)$ be
their exponential, where $C$ is the set of morphisms $Y\to X$ and $\gamma(f)$
is the set of realizers for $f$.

For modesty of $X^{Y}$, let $c_{0}\in\gamma(f)$ and $c_{1}\in\gamma(g)$ for
some $f,g\in C$ such that $c_{0}=c_{1}$. Given $y\in Y$ and $b\in\beta(y)$, we
have that $c_{0}(b)=c_{1}(b)$ and hence, by modesty of $X$, that $f(y)=g(y)$.
It follows that $f=g$ and $X^{Y}$ is modest.

Now suppose both $X$ and $Y$ are bases. To see that $X^{Y}$ is strongly
modest, let $c_{0},c_{1}\in\gamma(f)$. Given any $b\in B$, find $y\in Y$ such
that $b\in\beta(y)$. It follows that $c_{0}(b),c_{1}(b)\in\alpha(f(y))$. Hence
$c_{0}(b)=c_{1}(b)$ and therefore $c_{0}=c_{1}$ by extensionality.

Finally, by our assumptions and Lemma 3.3, we know that
$\bigcup\mathrm{Im}(\gamma)=|B\to A|$, and so, $X^{Y}$ is also exhaustive. ∎

######  Proposition 3.5.

If $\mathcal{T}$ is standard, then $N$ is a natural numbers object in
$\mathcal{T}$. Moreover, this natural numbers object is preserved by $E$.

###### Proof.

The natural numbers object in $\mathbf{Asm}$ is $(\mathbb{N},N,\nu)$ with
$\nu(n)=\left\\{\bar{n}\right\\}$, which coincides with $E(N)$ if
$\mathcal{T}$ is standard. And because $E$ is a full and faithful functor
preserving the terminal object, it reflects the natural numbers object. So $N$
is the natural numbers object in $\mathcal{T}$. ∎

###  3.2. IP, AC and MP

In this section, we investigate which common principles hold in the assemblies
$\mathbf{Asm}_{\mathcal{T}}$ for a given extensional tca $\mathcal{T}$.

######  Theorem 3.6.

If $\mathcal{T}$ is an extensional tca for which $|\bot|$ is inhabited, then
in the category of assemblies $\mathbf{Asm}_{\mathcal{T}}$ over that tca, the
following independence of premise principle is satisfied:

$(\neg\varphi\rightarrow\exists y^{Y}\ \psi(y))\rightarrow(\exists y^{Y}\
\neg\varphi\rightarrow\psi(y)),$

for all modest and exhaustive $Y$.

###### Proof.

Let $(X,A,\alpha)$ be the assembly that is the context of the independence of
premise principle and $(Y,B,\beta)$ an assembly which is both modest and
exhaustive. We will first calculate the predicates on $(X,A,\alpha)$ that
correspond to the premise and conclusion of IP. To fix notation, let
$(C,\gamma)={\llbracket\varphi\rrbracket}\in P(X)$ be the predicate
corresponding to ${\varphi}$, and $(D,\delta)={\llbracket\psi\rrbracket}\in
P(X\times Y)$ be the predicate corresponding to $\psi$. Then we may assume
that the interpretation of $\lnot\varphi$ will be $(A,\mu)$ with
$\mu(x)=\bigcup\\{\,\alpha(x)\,:\,\gamma(x)=\emptyset\\}$, by Lemma 2.17.

It is straightforward to compute that
${\llbracket\neg\varphi\rightarrow\exists y^{Y}\psi(y)\rrbracket}=(D^{A}\times
A,\theta)$, where $(m,n)\in\theta(x)$ if and only if $n\in\alpha(x)$ and
$m:A\to D$ is a morphism of types such that $i\in\mu(x)$ implies
$mi\in\bigcup_{y\in Y}\delta(x,y)$.

On the other hand, ${\llbracket\exists
y\,({\neg\varphi}\rightarrow\psi(y))\rrbracket}=(D^{A\times B}\times(A\times
B),\eta)$ such that $(k,l)\in\eta(x)$ if and only if there is some $y\in Y$
such that $l\in(\alpha\times\beta)(x,y)$ and $kj\in\delta(x,y)$ for any
$j\in\mu(x)\times\beta(y)$.

To show that the above principle of independence of premise holds, it suffices
to show that ${\llbracket\neg\varphi\rightarrow\exists
y^{Y}\psi(y)\rrbracket}\leq{\llbracket\exists
y(\neg\varphi\rightarrow\psi(y))\rrbracket}$. To do so, we have to provide a
morphism of types $f:D^{A}\times A\to D^{A\times B}\times(A\times B)$ such
that $(m,n)\in\theta(x)$ implies $f(m,n)\in\eta(x)$. As
${\llbracket\psi\rrbracket}$ is a predicate on $X\times Y$, there is a
morphism of types $g:D\to A\times B$ such that $i\in\delta(x,y)$ implies
$gi\in\alpha_{X\times Y}(x,y)=\alpha(x)\times\beta(y)$. Then take
$f(m,n):=(\lambda i.mn,(n,\mathsf{snd}(g(mn))))$. We have to show
$(m,n)\in\theta(x)$ implies $f(m,n)\in\eta(x)$.

So assume that $(m,n)\in\theta(x)$, i.e., $n\in\alpha(x)$ and $m:A\to D$ is a
morphism of types such that $i\in\mu(x)$ implies $mi\in\bigcup_{y\in
Y}\delta(x,y)$. We have $mn\in D$, $g(mn)\in A\times B$ and
$\mathsf{snd}(g(mn))\in B$. Since $Y$ is exhaustive, there is an $y\in Y$ with
$\mathsf{snd}(g(mn))\in\beta(y)$. So
$(n,\mathsf{snd}(g(mn)))\in(\alpha\times\beta)(x,y)$.

It remains to show that $mn\in\delta(x,y)$ whenever
$j\in\mu(x)\times\beta(y)$. But if $\mathsf{fst}\,j\in\mu(x)$, then
$\mu(x)=\alpha(x)$ and $n\in\alpha(x)$. So $mn\in\delta(x,y^{\prime})$ for
some $y^{\prime}\in Y$. We would like to have $y=y^{\prime}$, but this follows
because $\mathsf{snd}\,(g(mn))\in\beta(y^{\prime})$ and $Y$ is modest. ∎

######  Theorem 3.7.

Let $\mathcal{T}$ be an extensional tca. The category
$\mathbf{Asm}_{\mathcal{T}}$ satisfies the axiom of choice for all basic
assemblies. In particular, if $\mathcal{T}$ is also standard, we have the
axiom of choice in all finite types.

###### Proof.

Let $(X,A,\alpha)$ and $(Y,B,\beta)$ be basic assemblies, and $(Z,C,\gamma)$
be an arbitrary assembly. We will prove the axiom of choice for $X$ and $Y$ in
context $Z$:

$(\forall x^{X}\exists y^{Y}\ \varphi(x,y,z))\rightarrow(\exists f^{X\to
Y}\forall x^{X}\ \varphi(x,fx,z)).$

We will compute the predicates corresponding to the premise and conclusion of
the statement and then prove that the former is a subpredicate of the latter.
To do so, assume that $(D,\delta)={\llbracket\varphi(x,y,z)\rrbracket}\in
P(X\times Y\times Z)$ is witnessed by $\iota_{D}$.

It is then straightforward to compute that

${\llbracket\forall x^{X}\exists y^{Y}\ \varphi(x,y,z)\rrbracket}=(C\times
D^{A\times C},\eta),$

where $(n,m)\in\eta(z)$ if and only if $n\in\gamma(z)$ and $m:A\times C\to D$
is a morphism of types such that for every $k\in(\alpha\times\gamma)(x,z)$,
there is some $y\in Y$ with $mk\in\delta(x,y,z)$. Moreover, we compute that

${\llbracket\exists f^{X\to Y}\forall x^{X}\
\varphi(x,fx,z)\rrbracket}=((B^{A}\times C)\times(D\times(A\times B^{A}\times
C))^{A\times B^{A}\times C},\theta),$

where $(n,m)\in\theta(z)$ if and only if there is some $f\in Y^{X}$ such that
$n\in(\beta^{\alpha}\times\gamma)(f,z)$ and $m:A\times B^{A}\times C\to
D\times(A\times B^{A}\times C)$ is a morphism of types such that for all $x\in
X$ and $k\in(\alpha\times\beta^{\alpha}\times\gamma)(x,f,z)$ we have that
$mk\in\delta(x,fx,z)\times(\alpha\times\beta^{\alpha}\times\gamma)(x,f,z)$.

Let $z\in Z$ and $(n,m)\in\eta(z)$ be given, and define
$\check{f}_{n,m}:=\lambda j.\pi_{Y}(\iota_{D}(m(j,n)))$. It follows that
$\check{f}_{n,m}$ is a morphism of types from $A$ to $B$ as it is defined by a
$\lambda$-expression. By Lemma 3.3, there is a morphism $f_{n,m}:X\to Y$ of
assemblies which is tracked by $\check{f}$. Hence
$(\check{f},n)\in(\beta^{\alpha}\times\gamma)(f_{n,m},z)$.

Furthermore, let $x\in X$ be given and assume that
$k\in(\alpha\times\beta^{\alpha}\times\gamma)(x,f_{n,m},z)$. Then
$m(\pi_{X}k,n)\in\delta(x,y,z)$ for some $y\in Y$. Now since

$\check{f}_{n,m}(\pi_{X}k)=\pi_{Y}(\iota_{D}(m(\pi_{X}k,n))),$

it follows that $\check{f}_{n,m}(\pi_{X}k)\in\beta(y)$. By the fact that $Y$
is a base, it follows that $y=f_{n,m}x$. Hence,
$m(\pi_{X}k,n)\in\delta(x,f_{n,m}x,z)$.

The above reasoning shows that the following map does the job:

$\lambda(n,m).((\check{f}_{n,m},n),\lambda k.(m(\pi_{X}k,n),k))$

This map is clearly a morphism of types as it is defined as a
$\lambda$-expression. ∎

Let $\mathcal{T}$ be a consistent tca. We say that an element $f$ of type
$(N\times N)\to N$ _solves the halting problem_ if and only if the following
condition holds for all natural numbers $a$ and $b$:

$f(\bar{a},\bar{b})=\begin{cases}\mathsf{succ}\,\mathsf{0},&\text{ if the
machine $a$ halts on input $b$,}\\\ \mathsf{0},&\text{ otherwise.}\end{cases}$

For ease of notation we will write “$ab{\downarrow}$” to say that machine $a$
halts on input $b$, and “$ab{\uparrow}$” for the negation of the previous
statement.

######  Theorem 3.8.

Let $\mathcal{T}$ be an extensional and consistent tca that does not contain
an element solving the halting problem. If we assume Markov’s principle in the
metatheory, then Markov’s principle fails in $\mathbf{Asm}_{\mathcal{T}}$.

###### Proof.

Let $(\mathbb{N},N,\nu)$ be the natural numbers object. Let $T=(N\times
N\times N,\tau)$ be the predicate on the assembly
$\mathbb{N}\times\mathbb{N}\times\mathbb{N}$ defined by

$\tau(a,b,n)=\\{\langle\bar{a},\bar{b},\bar{n}\rangle\,:\,T(a,b,n)\\}$

where $T$ is Kleene’s $T$-predicate.

Suppose, for contradiction, that Markov’s principle holds on
$\mathbf{Asm}_{\mathcal{T}}$. It follows that
$(A,\alpha)={\llbracket\neg\neg\exists n\,T(a,b,n)\rrbracket}$ is a subobject
of $(B,\beta)={\llbracket\exists nH(a,b,n)\rrbracket}$. Note that
$\beta(a,b)=\\{\langle\bar{a},\bar{b},\bar{n}\rangle\,:\,T(a,b,n)\\}$ and
hence
$\alpha(a,b)=\\{\langle\bar{a},\bar{b},\bar{m}\rangle\,:\,\lnot\,\lnot\exists
n\in\mathbb{N}\,T(a,b,n)\\}$ by Lemma 2.17. Assuming Markov’s Principle in the
metatheory, this induces the existence of a morphism $g:N\times N\to N$ of
types such that if $T(a,b,n)$ for some $n$, then $T(a,b,g(a,b))$. This means
that $\exists n\,T(a,b,n)$ can be decided by checking $T(a,b,g(a,b))$; in
other words, the halting problem is decidable in $\mathcal{T}$. ∎

######  Remark 3.9.

We will recover the results in Chapter 2 of the MSc thesis of Mees de Vries
[10] if we restrict attention to the extensional tca of inhabited PERs over
$K_{1}$ (see also the next section). In the other chapters De Vries shows that
the resulting category of assemblies arises as the $\lnot\lnot$-separated
objects of a realizability topos which combines aspects of both the
extensional and modified realizability topos (for which, see [7]).

##  4\. Apartness assemblies and converse extensionality

In this section we will introduce a new extensional tca, which we will call
the _apartness types_ ; in fact, we will be able to define a tca of apartness
types for each consistent tca. Our main goal is to show that converse
extensionality principles will hold in the category of assemblies over the
apartness types.

_Throughout this section $\mathcal{T}$ will be a consistent typed combinatory
algebra._

###  4.1. Apartness types

In this section, we define a category of apartness types based on a typed
combinatory algebra. To motivate this definition, consider the following
constructions of _PERs_ over a tca $\mathcal{T}$.

######  Definition 4.1.

Let $\mathcal{T}$ be a consistent tca. The _category of PERs_ over
$\mathcal{T}$ is defined as follows: its objects are pairs $(A,R)$ where $A$
is a type in $\mathcal{T}$ and $R$ is a partial equivalence relation on $|A|$
(that is, a symmetric and transitive relation on $|A|$). The morphisms
$(A,R)\to(B,S)$ are equivalence classes of elements $f\in|A\to B|$ such that
$a_{0}Ra_{1}$ implies $fa_{0}Sfa_{1}$ for all $a_{0},a_{1}\in|A|$. Two such
elements $f,g\in|A\to B|$ will be considered equivalent if $faSga$ for each
$a\in|A|$ for which $aRa$ holds. The _inhabited PERs_ over $\mathcal{T}$ are
those PERs $(A,R)$ for which there is at least one element $a\in|A|$ such that
$aRa$.

One can check that the (inhabited) PERs form a well-pointed cartesian closed
category with a natural numbers object and weak finite sums. The apartness
types are a variation on this construction. The main idea is to replace the
partial equivalence relations by a notion of apartness, which is to be thought
of as a positive way of saying that two elements are inequivalent. And the
fact that the notion of apartness is positive means in particular that to
assert that two elements are apart requires evidence (it is “proof relevant”).
With this in mind, we have settled on the following definition.

######  Definition 4.2.

Let $\mathcal{T}$ be a consistent tca. A _$\mathcal{T}$ -apartness type_
$\mathcal{A}$ is a tuple $(A,T_{A},T^{-}_{A},\mathrel{\\#}_{A})$ consisting of
types $T_{A},T_{A}^{-}\in\mathcal{T}$, a subset $A\subseteq|T_{A}|$ and a
relation ${\mathrel{\\#}_{A}}\subseteq A\times A\times T_{A}^{-}$. Instead of
$(a_{0},a_{1},n)\in{\mathrel{\\#}_{A}}$ we will write
$n:a_{0}\mathrel{\\#}_{A}a_{1}$. We will require both $A$ and $|T_{A}^{-}|$ to
be inhabited. In addition, some conditions have to be satisfied:

  1. (i)

Reflexivity. There are no $a\in A$, $n\in A^{-}$ such that
$n:a\mathrel{\\#}_{A}a$.

  2. (ii)

Symmetry. There is $s\in|T_{A}\to T_{A}\to T_{A}^{-}\to T_{A}^{-}|$ such that
whenever $n:a_{0}\mathrel{\\#}_{A}a_{1}$, then
$sa_{0}a_{1}n:a_{1}\mathrel{\\#}_{A}a_{0}$.

  3. (iii)

Transitivity. There is $t\in|T_{A}\to T_{A}\to T_{A}\to
T_{A}^{-}\to(T_{A}^{-}+T_{A}^{-})|$ such that whenever
$n:a_{0}\mathrel{\\#}_{A}a_{1}$, then either
$ta_{0}a_{1}a_{2}n=\mathsf{inl}(m)$ and $m:a_{0}\mathrel{\\#}_{A}a_{2}$, or
$ta_{0}a_{1}a_{2}n=\mathsf{inr}(m)$ and $m:a_{1}\mathrel{\\#}_{A}a_{2}$.

For every apartness type $\mathcal{A}$ we can define an equivalence relation
$\sim_{A}$ on $A$ by saying:

$a_{0}\sim_{A}a_{1}\text{ if and only if there is no $n$ such that
}n:a_{0}\mathrel{\\#}_{A}a_{1}.$

######  Definition 4.3.

If $\mathcal{A}=(A,T_{A},T_{A}^{-},\mathrel{\\#}_{A})$ and
$\mathcal{B}=(B,T_{B},T_{B}^{-},\mathrel{\\#}_{B})$ are
$\mathcal{T}$-apartness types, then a _premorphism from $\mathcal{A}$ to
$\mathcal{B}$_ is an element $f\in|(T_{A}\to T_{B})\times(T_{A}\to T_{A}\to
T_{B}^{-}\to T_{A}^{-})|$ such that:

  1. (i)

$(\mathsf{fst}\,f)(a)\in B$ for all $a\in A$, and

  2. (ii)

for all $a_{0},a_{1}\in A$ and $n\in T_{B}^{-}$, if
$n:(\mathsf{fst}\,f)(a_{0})\mathrel{\\#}_{B}(\mathsf{fst}\,f)(a_{1})$, then
$(\mathsf{snd}\,f)a_{0}a_{1}n:a_{0}\mathrel{\\#}_{A}a_{1}$.

If $f$ is a premorphism, we will usually write $f$ for $\mathsf{fst}\,f$ and
$f^{-}$ for $\mathsf{snd}\,f$ without causing confusion. Note that for such a
premorphism, the map $f:A\to B$ preserves the equivalence relation $\sim$ by
condition (ii). We define an equivalence relation on premorphisms:

> $f\sim g$ if and only if $(\mathsf{fst}\,f)(a)\sim_{B}(\mathsf{fst}\,g)(a)$
> for all $a\in A$.

######  Definition 4.4.

The category $\mathbf{ApType}_{\mathcal{T}}$ of $\mathcal{T}$-apartness types
is the category whose objects are $\mathcal{T}$-apartness types and whose
morphisms are equivalence classes of $\mathcal{T}$-premorphisms.

######  Proposition 4.5.

The category $\mathbf{ApType}_{\mathcal{T}}$ of $\mathcal{T}$-apartness types
is a well-pointed cartesian closed category with a natural numbers object,
binary coproducts and a weak initial object.

###### Proof.

Let $(A,T_{A},T_{A}^{-},\mathrel{\\#}_{A})$ and
$(B,T_{B},T_{B}^{-},\mathrel{\\#}_{B})$ be $\mathcal{T}$-apartness types.
Their product can be computed as follows:

$(A,T_{A},T_{A}^{-},\mathrel{\\#}_{A})\times(B,T_{B},T_{B}^{-},\mathrel{\\#}_{B})=(A\times
B,T_{A}\times T_{B},T_{A}^{-}+T_{B}^{-},\mathrel{\\#}_{A\times B}),$

where

$A\times B=\\{\,x\in|T_{A}\times T_{B}|\,:\,\mathsf{fst}\,x\in
A,\mathsf{snd}\,x\in B\\}$

and $n:x_{0}\mathrel{\\#}_{A\times B}x_{1}$ if and only if either
$n=\mathsf{inl}(m)$ with
$m:\mathsf{fst}\,x_{0}\mathrel{\\#}_{A}\mathsf{fst},x_{1}$ or
$n=\mathsf{inr}(m)$ with
$m:\mathsf{snd}\,x_{0}\mathrel{\\#}_{B}\mathsf{snd}\,x_{1}$.

The exponential
$(B,T_{B},T_{B}^{-},\mathrel{\\#}_{B})\to(A,T_{A},T_{A}^{-},\mathrel{\\#}_{A})$
is $(E,T_{E},T_{E}^{-},\mathrel{\\#}_{E})$, where

$\displaystyle T_{E}$ $\displaystyle=(T_{B}\to T_{A})\times(T_{B}\to T_{B}\to
T_{A}^{-}\to T_{B}^{-}),$ $\displaystyle E$
$\displaystyle=\\{\,\text{premorphisms }B\to A\,\\},$ $\displaystyle
T_{E}^{-}$ $\displaystyle=T_{B}\times T_{A}^{-},$

and $n:f\mathrel{\\#}_{E}g$ if and only if $\mathsf{fst}\,n\in B$ and
$\mathsf{snd}\,n:f(\mathsf{fst}\,n)\mathrel{\\#}_{A}g(\mathsf{fst}\,n)$.

The natural numbers object $\mathcal{N}=(\mathcal{N},N,N,\mathrel{\\#}_{N})$
is defined as follows:

$\displaystyle\mathcal{N}$
$\displaystyle=\\{\,\overline{n}\,:\,n\in\mathbb{N}\\},\text{ and, }$
$\displaystyle x:n$ $\displaystyle\mathrel{\\#}_{N}m\text{ if and only if
}n\neq m.$

Establishing that this is indeed the natural numbers object makes use of the
primitive recursion operator $\mathsf{R}$ of the tca $\mathcal{T}$ at hand.

The following is the coproduct
$(A,T_{A},T_{A}^{-},\mathrel{\\#}_{A})+(B,T_{B},T_{B}^{-},\mathrel{\\#}_{B})$:

$(A+B,T_{A}+T_{B},T_{A}^{-}\times T_{B}^{-},\mathrel{\\#}_{A+B}),$

where $A+B=\\{\mathsf{inl}\,a\,:\,a\in A\\}\cup\\{\mathsf{inr}\,b\,:\,b\in
B\\}$ and $n:\mathsf{inl}\,a_{0}\mathrel{\\#}_{A+B}\mathsf{inl}\,a_{1}$ if
$\mathsf{fst}\,n:a_{0}\mathrel{\\#}_{A}a_{1}$,
$n:\mathsf{inr}\,b_{0}\mathrel{\\#}_{A+B}\mathsf{inr}\,b_{1}$ if
$\mathsf{snd}\,n:b_{0}\mathrel{\\#}_{A}b_{1}$, while
$n:\mathsf{inl}\,a\mathrel{\\#}_{A+B}\mathsf{inr}\,b$ and
$n:\mathsf{inr}\,b\mathrel{\\#}_{A+B}\mathsf{inl}\,a$ are always true.

Finally, the apartness types have a terminal object $\mathbf{1}$, explicitly
calculated as $(\left\\{\mathsf{t}\right\\},\top,\top,\emptyset)$; this object
is also weakly initial. ∎

######  Corollary 4.6.

Let $\mathcal{T}$ be a consistent tca. The apartness types
$\mathbf{ApType}_{\mathcal{T}}$ form an extensional and standard tca in which
$|\bot|$ is inhabited.

###### Proof.

This is immediate from the previous proposition and Example 2.6(v). Note that
$\mathbf{ApType}_{\mathcal{T}}$ is standard by construction and that
$|\mathcal{A}|=A/{\sim}$ for any apartness type $\mathcal{A}$. ∎

######  Lemma 4.7.

If $\mathbf{ApType}_{\mathcal{T}}$ has a functional solving the halting
problem, then so does $\mathcal{T}$.

###### Proof.

If $f$ solves the halting problem in $\mathbf{ApType}_{\mathcal{T}}$, then
$\mathsf{fst}\,f$ solves the halting problem in $\mathcal{T}$. ∎

######  Definition 4.8.

Let $\mathcal{T}$ be a tca. The _category $\mathbf{ApAsm}_{\mathcal{T}}$ of
$\mathcal{T}$-apartness assemblies_ is the category
$\mathbf{Asm}_{\mathbf{ApType}_{\mathcal{T}}}$ of
$\mathbf{ApType}_{\mathcal{T}}$-assemblies.

######  Remark 4.9.

Note that the existence of a universal type on $\mathbf{ApType}_{\mathcal{T}}$
induces a universal type on $\mathcal{T}$. With [4, Proposition 2.5] it
follows that $\mathbf{ApType}_{\mathcal{K}_{1}}$ and
$\mathbf{ApType}_{\mathcal{K}_{2}^{\mathrm{rec}}}$ do not have universal
types. By [4, Theorem 4.2], this means that the ex/reg-completion of the
apartness assemblies $\mathbf{ApAsm}_{\mathcal{K}_{1}}$ and
$\mathbf{ApAsm}_{\mathcal{K}_{2}^{\mathrm{rec}}}$ are not toposes.

###  4.2. Converse extensionality

Our next aim is to show that in the apartness assemblies certain _converse
extensionality principles_ $\mathsf{CE}_{n}$ hold:

$\exists X^{n+2\to n+1\to n+1\to n}\forall\Phi^{n+2}\forall f^{n+1},g^{n+1}\
(\Phi f\neq_{0}\Phi g\rightarrow f(X\Phi fg)\neq_{0}g(X\Phi fg)).$

Given a strongly modest apartness assembly $(X,A,\alpha)$ and $x\in X$, we
write $\check{x}$ for the unique realizer of $x$, i.e.,
$\check{x}\in\alpha(x)$. Recall that all finite types are strongly modest, so
we will make plenty of use of this convention.

######  Theorem 4.10.

If $\mathcal{T}$ is a consistent tca, then converse extensionality
$\mathsf{CE}_{0}$ holds in $\mathbf{ApAsm}_{\mathcal{T}}$.

###### Proof.

Given a finite type $\tau$, we will write $(X_{\tau},A_{\tau},\alpha_{\tau})$
for ${\llbracket\tau\rrbracket}$. Moreover, we will abbreviate the type $2\to
1\to 1\to 0$ with $\sigma$. It is then straightforward to compute that

${\llbracket\Phi f\neq_{0}\Phi g\rrbracket}=(A_{2}\times A_{1}\times
A_{1}\times A_{\sigma},\alpha),$

where

$\alpha(\Phi,f,g,X)=\begin{cases}(\alpha_{2}\times\alpha_{1}\times\alpha_{1}\times\alpha_{\sigma})(\Phi,f,g,X),&\text{
if }\Phi f\neq\Phi g,\\\ \emptyset,&\text{ otherwise,}\end{cases}$

and

${\llbracket f(X\Phi fg)\neq_{0}g(X\Phi fg))\rrbracket}=(A_{2}\times
A_{1}\times A_{1}\times A_{\sigma},\beta),$

where

$\beta(\Phi,f,g,X)=\begin{cases}(\alpha_{2}\times\alpha_{1}\times\alpha_{1}\times\alpha_{\sigma})(\Phi,f,g,X),&\text{
if }f(X\Phi fg)\neq g(X\Phi fg),\\\ \emptyset,&\text{ otherwise.}\end{cases}$

We then conclude that

$\displaystyle{\llbracket\exists X^{\sigma}\ (\Phi f\neq_{0}\Phi g\rightarrow
f(X\Phi fg)\neq_{0}g(X\Phi fg))\rrbracket}$ $\displaystyle\hskip
28.45274pt=((A_{2}\times A_{1}\times A_{1}\times A_{\sigma})^{(A_{2}\times
A_{1}\times A_{1}\times A_{\sigma})}\times(A_{2}\times A_{1}\times A_{1}\times
A_{\sigma}),\delta),$

where $(m,k)\in\delta(\Phi,f,g)$ if and only if there is some $X\in
X_{\sigma}$ such that
$k\in(\alpha_{2}\times\alpha_{1}\times\alpha_{1}\times\alpha_{\sigma})(\Phi,f,g,X)$
and $m:A_{2}\times A_{1}\times A_{1}\times A_{\sigma}\to A_{2}\times
A_{1}\times A_{1}\times A_{\sigma}$ is a morphism of types such that if
$j\in\alpha(\Phi,f,g,X)$ then $mj\in\beta(\Phi,f,g,X)$.

We will show that

${\llbracket\exists X^{\sigma}\ (\Phi f\neq_{0}\Phi g\rightarrow f(X\Phi
fg)\neq_{0}g(X\Phi fg))\rrbracket}$

is the maximal element in $P({\llbracket 2\rrbracket}\times{\llbracket
1\rrbracket}\times{\llbracket 1\rrbracket})$. This suffices to show that
$\mathsf{CE}_{0}$ holds by a repeated application of the axiom of choice,
Theorem 3.7.

To this end, we will construct a morphism $F:\mathcal{T}_{2\times 1\times
1}\to\mathcal{T}_{2\times 1\times 1\times\sigma}^{\mathcal{T}_{2\times 1\times
1\times\sigma}}\times\mathcal{T}_{2\times 1\times 1\times\sigma}$ such that
$i\in\alpha_{2\times 1\times 1}(\Phi,f,g)$ implies that
$Fi\in\delta(\Phi,f,g)$.

We let $F(\check{\Phi},\check{f},\check{g})=(\mathsf{id}_{2\times 1\times
1\times\sigma},(\check{\Phi},\check{f},\check{g},\check{X}))$, where
$\check{X}$ is an implementation of the following informally described
algorithm: Let $(\check{\Phi},\check{f},\check{g})\in\mathcal{T}_{2\times
1\times 1}$. By Lemma 2.7, we can check whether
$\check{\Phi}\check{f}=\check{\Phi}\check{g}$. If this is the case, return
$0$. If this is not the case, compute the least natural number
$\check{x}\leq\mathsf{fst}\,(\check{\Phi}^{-}(\check{f},\check{g},\mathsf{0}))$
such that $\check{f}\check{x}\neq\check{g}\check{x}$, and return $\check{x}$.
To understand this, observe that
$\check{\Phi}^{-}(\check{f},\check{g},\mathsf{0})$ is a witness for the fact
that $\check{f}$ and $\check{g}$ are apart. Therefore
$\mathsf{fst}\,(\check{\Phi}^{-}(\check{f},\check{g},\mathsf{0}))$ is an
element $\check{y}$ such that $\check{f}\check{y}\not=\check{g}\check{y}$, and
$\check{x}$ is the smallest such. Note that $\check{x}$ depends on $\check{f}$
and $\check{g}$ only, not on $\check{\Phi}^{-}$.

We will first argue that $F$ is a morphism of types and then show that it
establishes the desired result.

For the first part, we have to show that there is a map $F^{-}$ that witnesses
reflection of apartness, i.e., if
$m:F(\check{\Phi}_{0},f_{0},g_{0})\mathrel{\\#}F(\check{\Phi}_{1},f_{1},g_{1})$
then

$F^{-}((\check{\Phi}_{0},\check{f}_{0},\check{g}_{0}),(\check{\Phi}_{1},\check{f}_{1},\check{g}_{1}),m):(\check{\Phi}_{0},\check{f}_{0},\check{g}_{0})\mathrel{\\#}(\check{\Phi}_{1},\check{f}_{1},\check{g}_{1}).$

We define $F^{-}$ as follows. As the first projection of $F$ is constant, it
follows that $m=\mathsf{in}_{1}(n)$ such that
$n:(\check{\Phi}_{0},\check{f}_{0},\check{g}_{0},\check{X}_{0})\mathrel{\\#}(\check{\Phi}_{1},\check{f}_{1},\check{g}_{1},\check{X}_{1})$.
Hence, $n=\mathsf{in}_{i}(n_{i})$ for some $i\leq 3$.

If $i=0$, $i=1$ or $i=2$, we have found a witness for the apartness of the
$i$-th component and can thus just return $n$. If $i=3$, we have
$n_{3}:\check{X}_{0}\mathrel{\\#}\check{X}_{1}$. However, $\check{X}_{0}$ and
$\check{X}_{1}$ are codes for the same morphism, and hence they cannot be
apart. It is tedious but straightforward to check that $\check{X}$ is indeed a
morphism.

All we need to do to finish the proof is to show that $F$ indeed witnesses
that ${\llbracket\exists X^{\sigma}\ (\Phi f\neq_{0}\Phi g\rightarrow f(X\Phi
fg)\neq_{0}g(X\Phi fg))\rrbracket}$ is the maximal element of $P({\llbracket
2\rrbracket}\times{\llbracket 1\rrbracket}\times{\llbracket 1\rrbracket})$. So
let $(\check{\Phi},\check{f},\check{g})\in\alpha_{2\times 1\times
1}(\Phi,f,g)$. We have to show that
$F(\check{\Phi},\check{f},\check{g})\in\delta(\Phi,f,g)$: If $\Phi f=\Phi g$
this is trivially the case, so assume that $\Phi f\neq\Phi g$. Then it must
hold that $f\neq g$ and hence that there is some minimal $x\in\mathbb{N}$ with
$f(x)\neq g(x)$. By the definition of $F$, $\check{X}$ will calculate a
realizer $\check{x}$ of $x$. We therefore have that $k\in\alpha_{2\times
1\times 1\times\sigma}$. The condition on $m$ is satisfied by the fact that
$fx\neq gx$. ∎

######  Remark 4.11.

In particular, in the apartness assemblies over Gödel’s $T$ (considered as a
tca) the converse extensionality principle $\mathsf{CE}_{0}$ holds. This
should be contrasted with Howard’s negative result [8] saying that there is no
term in Gödel’s $T$ witnessing $\mathsf{CE}_{0}$ directly. The reason for this
discrepancy is that in the apartness types any type 2 functional $\Phi$ comes
with a functional $\Phi^{-}$ witnessing the fact that $\Phi$ reflects
apartness. This means that as soon as we discover that $\Phi f\not=\Phi g$ we
can find a natural number $y$ such that $fy\not=gy$; in particular, we can
find the least such $y$. Clearly, this $y$ could also have been found using
unbounded search, would this be available. But having one such $y$ available
means that the least such $y$ can be found using bounded search; as a result,
the least such $y$ can be found in the apartness types over any tca, including
those tcas where unbounded search is not available, like the term model of
Gödel’s $T$.

The same technique cannot be straightforwardly used to prove the converse
extensionality principle for higher types. The reason is that, despite the
fact that every function comes with a witness for the reflection of apartness
that we have access to, the functional $X$ will have to be extensional, so its
output cannot depend on which specific witness it was given as part of its
input. With certain tca’s, it is however possible to succeed with a slight
modification.

######  Definition 4.12.

We say that $\mathcal{T}$ has a _modulus of continuity_ if there is a
functional $M$ of type $2\to 1\to 0$ in $\mathcal{T}$ such that for every
$f^{2}$ and $x^{1},y^{1}$, we have that if
$x\upharpoonright(Mfx)=y\upharpoonright(Mfx)$, then $fx=fy$. (Here
$x\upharpoonright n$ refers to the finite sequence consisting of the first $n$
elements of $x$; that is, $\langle x(0),x(1),\ldots,x(n-1)\rangle$.)

######  Theorem 4.13.

If $\mathcal{T}$ is a consistent tca with a modulus of continuity, then
converse extensionality $\mathsf{CE}_{1}$ holds in
$\mathbf{ApAsm}_{\mathcal{T}}$.

###### Proof.

The proof is essentially the same as the proof of the previous theorem with a
slight modification in the algorithm needed for accommodating the higher types
we deal with here. For that reason, we will only state the modified algorithm
and leave the details to the reader.

Let $\sigma=3\to 2\to 2\to 1$, and $M$ be the modulus of continuity of
$\mathcal{T}$. We apply the same notational convention as in the previous
proof, i.e. ${\llbracket\tau\rrbracket}=(X_{\tau},A_{\tau},\alpha_{\tau})$ for
any finite type $\tau$. Analogous to the situation in the previous proof, we
need to provide a morphism of types $F:(A_{3}\times A_{2}\times
A_{2})\to(A_{3}\times A_{2}\times A_{2}\times A_{1})^{(A_{3}\times A_{2}\times
A_{2}\times A_{1})}\times(A_{3}\times A_{2}\times A_{2}\times A_{\sigma})$
witnessing that

${\llbracket\exists X^{\sigma}\ (\Phi f\neq_{0}\Phi g\rightarrow f(X\Phi
fg)\neq_{0}g(X\Phi fg))\rrbracket}$

is maximal in $P({\llbracket 3\rrbracket}\times{\llbracket
2\rrbracket}\times{\llbracket 2\rrbracket})$. Having establish this fact, a
repeated application of the axiom of choice, Theorem 3.7, gives the desired
result.

We now informally describe the algorithm that implements $\check{X}$ as
follows. Fix a computable bijection $h:\mathbb{N}\to\mathbb{N}^{<\mathbb{N}}$.
Let $(\check{\Phi},\check{f},\check{g})\in A_{3}\times A_{2}\times A_{2}$ be
given. By Lemma 2.7, we can check whether
$\check{\Phi}\check{f}=\check{\Phi}\check{g}$. If this is the case, return
$\lambda n.0$. If this is not the case, proceed as follows: Compute
$b=\mathsf{fst}(\check{\Phi}^{-}(\check{f},\check{g},\mathsf{0}))$, and search
through all sequences $s$ of length $\leq\max(M\check{f}b,M\check{g}b)$ using
the ordering induced by $h$ until $\check{f}s^{*}\neq\check{g}s^{*}$, where

$s^{*}n=\begin{cases}s(n),&n<\mathsf{length}(s),\\\ 0,&\text{otherwise}.\\\
\end{cases}$

It is straightforward to check that $\check{X}$ gives rise to a morphism of
types.

Finally, define $F$ as the following map:

$(\check{\Phi},\check{f},\check{g})\mapsto(\mathsf{id}_{3\times 2\times
2\times\sigma},\check{X}).$

As in the proof of the previous theorem, it is straightforward to check that
$F$ is well-defined, a morphism of types, and witnesses the maximality of the
existential statement in $P({\llbracket 3\rrbracket}\times{\llbracket
2\rrbracket}\times{\llbracket 2\rrbracket})$. ∎

We apply the results of this section to some specific tca’s.

######  Corollary 4.14.

  1. (i)

Let $\mathcal{K}_{1}$ be the tca arising from Kleene’s first model. Then,
$\mathbf{ApAsm}_{\mathcal{K}_{1}}\vDash\mathsf{IP}+\mathsf{AC}+\mathsf{CE}_{0}$
but $\mathbf{ApAsm}_{\mathcal{K}_{1}}\not\vDash\mathsf{MP}$.

  2. (ii)

Let $\mathcal{K}_{2}^{\mathrm{rec}}$ be the recursive submodel of Kleene’s
second algebra $\mathcal{K}_{2}$. Then,
$\mathbf{ApAsm}_{\mathcal{K}_{2}^{\mathrm{rec}}}\vDash\mathsf{IP}+\mathsf{AC}+\mathsf{CE}_{0}+\mathsf{CE}_{1}$
but $\mathbf{ApAsm}_{\mathcal{K}_{2}^{\mathrm{rec}}}\not\vDash\mathsf{MP}$.

###### Proof.

Note that both $\mathcal{K}_{1}$ and $\mathcal{K}_{2}^{\mathrm{rec}}$ do not
contain an element solving the halting problem: both tca’s contain only
recursive functions. Furthermore, note that $\mathcal{K}_{2}^{\mathrm{rec}}$
has a modulus of continuity by [8, Theorem 2.6.3]; note that the functional
constructed there for $\mathcal{K}_{2}$ also exists in
$\mathcal{K}_{2}^{\mathrm{rec}}$ as it is a computable function. Then apply
Theorems 3.6, 3.7, 3.8, 4.10 and 4.13 and Lemma 4.7. ∎

######  Remark 4.15.

Note that ${\textsf{E-HA}}^{\omega}+\mathsf{AC}+\mathsf{MP}$ proves
$\mathsf{CE}_{0}$. Indeed, if $\mathsf{MP}_{n}$ is Markov’s principle for
objects of type $n$, then
${\textsf{E-HA}}^{\omega}+\mathsf{AC}+\mathsf{MP}_{n}\vdash\mathsf{CE}_{n}$,
as the following calculation shows:

where $\mathsf{EXT}$ stands for the axiom of extensionality and IL for
intuitionistic logic. So what the previous corollary shows is that the
implication cannot be reversed, in that
${\textsf{E-HA}}^{\omega}+\mathsf{AC}+\mathsf{CE}_{n}\not\vdash\mathsf{MP}_{n}$
for $n=0,1$.

######  Remark 4.16.

Reasoning classically, a stronger result is possible, as pointed out to us by
Ulrich Kohlenbach. Using modified realizability in ECF, we obtain a model of
${\textsf{E-HA}}^{\omega}+\mathsf{IP}+\mathsf{AC}+\mathsf{CE}_{n}+\lnot\mathsf{MP}$.
Under this interpretation, Markov’s principle fails because witnessing

$\forall f^{1}\,(\neg\neg\exists n^{0}\,f(n)=0\to\exists n^{0}\,f(n)=0)$

requires a discontinous functional. In addition, in ECF there are functionals
witnessing $\mathsf{CE}_{n}$ (see [8, Appendix]).

##  5\. Conclusion and directions for future research

We set out to witness the converse extensionality principles $\mathsf{CE}_{n}$
using Brouwer’s notion of apartness. We have succeeded in witnessing
$\mathsf{CE}_{0}$ using a modified realizability interpretation using
apartness types. The interesting aspect of this fact is that we can find this
witness in Gödel’s $T$, despite Howard’s result saying that $\mathsf{CE}_{0}$
cannot be directly witnessed in the term model. Witnessing higher
$\mathsf{CE}_{n}$ proved difficult, because we have to make sure that the
witnessing functional $X$ is still an extensional function. One natural
direction, then, might be to drop the requirement that the witnessing
functional $X$ be extensional.

As suggested to us by Ulrich Kohlenbach, it may also be interesting to use
enrichment of data to witness restricted forms of extensionality. For
instance, in proof mining one often needs extensionality in the form

$x=_{X}p\land T(p)=_{X}p\to T(x)=_{X}x,$

where $(X,d)$ is some metric space. Even when there are no functionals
witnessing full extensionality, functionals witnessing such restricted forms
of extensionality might exist (see, for instance, [3]).

Finally, another open question is whether the apartness assemblies arise as
subcategory of a suitable realizability topos.

## References

  * [1] E. Darpö and M.S. Mitrović  “Some results in constructive semigroup theory” arXiv:2103.07105, 2021
  * [2] U. Kohlenbach  “Applied proof theory: proof interpretations and their use in mathematics”, Springer Monographs in Mathematics  Springer-Verlag, Berlin, 2008, pp. xx+532
  * [3] U. Kohlenbach, L. Leuştean and A. Nicolae  “Quantitative results on Fejér monotone sequences”  In _Commun. Contemp. Math._ 20.2, 2018, pp. 175001542  DOI: 10.1142/S0219199717500158
  * [4] P. Lietz and T. Streicher  “Impredicativity entails untypedness”  In _Mathematical Structures in Computer Science_ 12.3 Cambridge University Press, 2002, pp. 335–347  DOI: 10.1017/S0960129502003663
  * [5] J.R. Longley  “Unifying typed and untyped realizability” Unpublished manuscript available from https://homepages.inf.ed.ac.uk/jrl/Research/unifying.txt, 1999
  * [6] J.R. Longley and D. Normann  “Higher-order computability”, Theory and Applications of Computability  Springer, Heidelberg, 2015, pp. xvi+571  DOI: 10.1007/978-3-662-47992-6
  * [7] J. Oosten  “Realizability: an introduction to its categorical side” 152, Studies in Logic and the Foundations of Mathematics  Elsevier B. V., Amsterdam, 2008, pp. xvi+310
  * [8] “Metamathematical investigation of intuitionistic arithmetic and analysis”, Lecture Notes in Mathematics, Vol. 344  Springer-Verlag, Berlin-New York, 1973, pp. xvii+485
  * [9] A.. Troelstra and D. Dalen  “Constructivism in mathematics. Vol. II” An introduction 123, Studies in Logic and the Foundations of Mathematics  North-Holland Publishing Co., Amsterdam, 1988, pp. i–xviii and 345–880 and I–LII
  * [10] M. Vries  “An extensional modified realizability topos” Available from https://eprints.illc.uva.nl/1568/1/MoL-2017-27.text.pdf, 2017

##  Appendix A A proof-theoretic account

Some of the results in this paper can also be stated in proof-theoretic
language. We include those statements here for the benefit of those readers
who are primarily interested in the proof-theoretic aspects of our work.

Let us work in ${\textsf{E-HA}}^{\omega}$ where we include both binary sum and
product types in the type structure. By induction on this type structure we
define for each finite type $\sigma$ two finite types $\sigma^{+}$ and
$\sigma^{-}$, as well as two formulas ${\rm dom}_{\sigma}$ and ${\rm
app}_{\sigma}$ in the language of ${\textsf{E-HA}}^{\omega}$ where ${\rm
dom}_{\sigma}$ has one free variable $x$ of type $\sigma^{+}$ and ${\rm
app}_{\sigma}$ has free variables $x,y,z$ of types $\sigma^{+},\sigma^{+}$ and
$\sigma^{-}$, respectively. (Here ${\rm dom}_{\sigma}$ stands for the “domain”
of $\sigma$: it applies to those elements of type $\sigma^{+}$ which are
suitable for interpreting elements of type $\sigma$. The predicate ${\rm
app}_{\sigma}(x,y,z)$ should be read as: $z$ is evidence for the statement
that $x$ and $y$ are apart; the variable $z$ is of type $\sigma^{-}$, so
$\sigma^{-}$ is the type of evidence of elements of type $\sigma$ being
apart.)

$\displaystyle N^{+}$ $\displaystyle:\equiv$ $\displaystyle N$ $\displaystyle
N^{-}$ $\displaystyle:\equiv$ $\displaystyle N$ $\displaystyle{\rm dom}_{N}$
$\displaystyle:\equiv$ $\displaystyle x=_{0}x$ $\displaystyle{\rm app}_{N}$
$\displaystyle:\equiv$ $\displaystyle x\not=y$
$\displaystyle(\sigma\times\tau)^{+}$ $\displaystyle:\equiv$
$\displaystyle\sigma^{+}\times\tau^{+}$ $\displaystyle(\sigma\times\tau)^{-}$
$\displaystyle:\equiv$ $\displaystyle\sigma^{-}+\tau^{-}$ $\displaystyle{\rm
dom}_{\sigma\times\tau}$ $\displaystyle:\equiv$ $\displaystyle{\rm
dom}_{\sigma}(\mathsf{fst}\,x)\land{\rm dom}_{\tau}(\mathsf{snd}\,x)$
$\displaystyle{\rm app}_{\sigma\times\tau}$ $\displaystyle:\equiv$
$\displaystyle\big{(}\,\exists u^{\sigma^{-}}\,(z=\mathsf{inl}\,u\land{\rm
app}_{\sigma}(\mathsf{fst}\,x,\mathsf{fst}\,y,u))\lor$ $\displaystyle\exists
v^{\tau^{-}}\,(z=\mathsf{inr}\,v\land{\rm
app}_{\sigma}(\mathsf{snd}\,x,\mathsf{snd}\,y,v))\,\big{)}$
$\displaystyle\land{\rm dom}_{\sigma\times\tau}(x)\land{\rm
dom}_{\sigma\times\tau}(y)$ $\displaystyle(\sigma+\tau)^{+}$
$\displaystyle:\equiv$ $\displaystyle\sigma^{+}+\tau^{+}$
$\displaystyle(\sigma+\tau)^{-}$ $\displaystyle:\equiv$
$\displaystyle\sigma^{-}\times\tau^{-}$ $\displaystyle{\rm dom}_{\sigma+\tau}$
$\displaystyle:\equiv$ $\displaystyle\exists
u^{\sigma^{+}}(x=\mathsf{inl}\,u\land{\rm dom}_{\sigma^{+}}(u))\lor\exists
v^{\tau^{+}}(x=\mathsf{inr}\,v\land{\rm dom}_{\tau^{+}}(v))$
$\displaystyle{\rm app}_{\sigma+\tau}$ $\displaystyle:\equiv$
$\displaystyle\big{(}\,\exists
u^{\sigma^{+}},v^{\tau^{+}}\,\big{(}\,(x=\mathsf{inl}\,u\land
y=\mathsf{inr}\,v)\lor(x=\mathsf{inr}\,v\land y=\mathsf{inl}\,u)\big{)}\lor$
$\displaystyle\exists u^{\sigma^{+}},v^{\sigma^{+}}\,(\,x=\mathsf{inl}\,u\land
y=\mathsf{inl}\,v\land{\rm app}_{\sigma^{+}}(u,v,\mathsf{fst}\,z))\lor$
$\displaystyle\exists u^{\tau^{+}},v^{\tau^{+}}\,(\,x=\mathsf{inr}\,u\land
y=\mathsf{inr}\,v\land{\rm
app}_{\tau^{+}}(u,v,\mathsf{snd}\,z))\,\big{)}\land$ $\displaystyle{\rm
dom}_{\sigma+\tau}(x)\land{\rm dom}_{\sigma+\tau}(y)$
$\displaystyle(\sigma\to\tau)^{+}$ $\displaystyle:\equiv$
$\displaystyle(\sigma^{+}\to\tau^{+})\times(\sigma^{+}\to\sigma^{+}\to\tau^{-}\to\sigma^{-})$
$\displaystyle(\sigma\to\tau)^{-}$ $\displaystyle:\equiv$
$\displaystyle\sigma^{+}\times\tau^{-}$ $\displaystyle{\rm
dom}_{\sigma\to\tau}$ $\displaystyle:\equiv$ $\displaystyle\forall
u^{\sigma^{+}}(\,{\rm dom}_{\sigma}(u)\to{\rm
dom}_{\tau}((\mathsf{fst}\,x)u)\,)\land$ $\displaystyle\forall
u^{\sigma^{+}},v^{\sigma^{+}},w^{\tau^{-}}\,(\,{\rm
app}_{\tau}((\mathsf{fst}\,x)(u),(\mathsf{fst}\,x)(v),w)\to$
$\displaystyle{\rm app}_{\sigma}(u,v,(\mathsf{snd}\,x)uvw)\,)$
$\displaystyle{\rm app}_{\sigma\to\tau}$ $\displaystyle:\equiv$
$\displaystyle{\rm dom}_{\sigma}(\mathsf{fst}\,z)\land{\rm
app}_{\tau}((\mathsf{fst}\,x)(\mathsf{fst}\,z),(\mathsf{fst}\,y)(\mathsf{fst}\,z),\mathsf{snd}\,z)$
$\displaystyle\land{\rm dom}_{\sigma\to\tau}(x)\land{\rm
dom}_{\sigma\to\tau}(y)$

Now we the following statements are provable in ${\textsf{E-HA}}^{\omega}$ for
each type $\sigma$:

  1. (i)

If ${\rm app}_{\sigma}(x,y,z)$, then ${\rm dom}_{\sigma}(x)$ and ${\rm
dom}_{\sigma}(y)$.

  2. (ii)

If ${\rm dom}_{\sigma}(x)$, then there is no $z$ such that ${\rm
app}_{\sigma}(x,x,z)$.

  3. (iii)

There is a functional $s:\sigma^{+}\to\sigma^{+}\to\sigma^{-}\to\sigma^{-}$,
such that if ${\rm app}_{\sigma}(x,y,z)$, then ${\rm app}_{\sigma}(y,x,sz)$.

  4. (iv)

There is a functional
$t:\sigma^{+}\to\sigma^{+}\to\sigma^{+}\to\sigma^{-}\to(\sigma^{-}+\sigma^{-})$
such that whenever ${\rm app}_{\sigma}(x,y,u)$ and ${\rm dom}_{\sigma}(z)$,
then either there is some $v$ such that $txyzu=\mathsf{inl}\,v$ and ${\rm
app}_{\sigma}(x,z,v)$ or there is some $w$ such that $txyzu=\mathsf{inr}\,w$
and ${\rm app}_{\sigma}(y,z,w)$.

We can define an interpretation $\alpha$ of ${\textsf{E-HA}}^{\omega}$ inside
${\textsf{E-HA}}^{\omega}$ where we interpret the elements of type $\sigma$ as
those elements $x$ of type $\sigma^{+}$ for which ${\rm dom}_{\sigma}(x)$
holds; two such elements $x$ and $y$ will be regarded as equal whenever there
is no $z$ such that ${\rm app}_{\sigma}(x,y,z)$ holds.

######  Theorem A.1.

The interpretation $\alpha$ gives us an interpretation of
${\textsf{E-HA}}^{\omega}+\mathsf{CE}_{0}$ inside ${\textsf{E-HA}}^{\omega}$.

Very rougly, the reason why the interpretation $\alpha$ witnesses
$\mathsf{CE}_{0}$ is that while elements of type $1=N\to N$ are interpreted as
the elements of type $1$ from the interpreting system (the extra information
they are endowed with is vacuous), elements $\Phi$ of type $2=(N\to N)\to N$
are endowed with the additional information that finds a point $x$ such that
$fx\not=gx$ as soon as $\Phi f\not=\Phi g$.

######  Corollary A.2.

By combining the interpretation $\alpha$ with modified realizability mr as
follows

${{\textsf{E-HA}}^{\omega}}$${{\textsf{E-HA}}^{\omega}}$${{\textsf{E-HA}}^{\omega},}$mr$\scriptstyle{\alpha}$

we obtain an interpretation of
${\textsf{E-HA}}^{\omega}+\mathsf{CE}_{0}+\mathsf{AC}+\mathsf{IP}$ inside
${\textsf{E-HA}}^{\omega}$.