# Sets completely separated by functions in Bishop Set Theory

Iosif Petrakis
Mathematics Institute, Ludwig-Maximilians-Universität München
<EMAIL_ADDRESS>
###### Abstract

Within Bishop Set Theory, a reconstruction of Bishop’s theory of sets, we
study the so-called completely separated sets, that is sets equipped with a
positive notion of an inequality, induced by a given set of real-valued
functions. We introduce the notion of a global family of completely separated
sets over an index-completely separated set, and we describe its Sigma- and
Pi-set. The free completely separated set on a given set is also presented.
Purely set-theoretic versions of the classical Stone-Čech theorem and the
Tychonoff embedding theorem for completely regular spaces are given, replacing
topological spaces with function spaces and completely regular spaces with
completely separated sets.
Keywords: constructive mathematics, Bishop set theory, apartness relation

##  1 Introduction

Constructive mathematics $(\mathrm{CM})$, although hard to define, is not only
mathematics within intuitionisitic logic. It also encompasses certain
“attitudes” towards the definition of mathematical concepts, in order to
reveal the computational content of mathematical proofs of theorems concerning
these concepts. Some of these attitudes, which are not uniformly and
consistently followed by the practitioners of $\mathrm{CM}$ though, are the
following:

  * •

Predicativity, that is the avoidance of circular, or impredicative
definitions, which often amounts to the avoidance of quantification over
proper classes in the definition of a mathematical concept.

  * •

The addition of witnessing information so that even weak choice principles,
such as countable choice111An approach to $\mathrm{CM}$ without countable
choice was spearheaded by Richman [44]., are avoided in proofs. Bishop’s
moduli of convergence, of continuity, of differentiability etc., in [3] are
examples of added witnesses to convergence, continuity, differentiability etc.

  * •

Preference for positive definitions of concepts over negative ones, that is
definitions using negation. The most characteristic example of the positive
approach to mathematical concepts within $\mathrm{CM}$, which goes back to
Brouwer, is the notion of inequality, or apartness relation on a set.

  * •

Preference for function-based concepts over set-based ones, as functions suit
better to $\mathrm{CM}$ than sets. Characteristic examples of this attitude
are the definition of an integrable complemented set through the integrability
of its partial characteristic function in constructive measure theory (see [4,
5]) and the reduction of the topology of open sets to the topology of
functions in constructive topology of Bishop spaces (see [6, 13], [24]-[36]
and [41]).

In this paper we highlight the combination of the last two attitudes in the
study of sets with an inequality, determined in a positive way from a given
set of functions. As many results shown here reveal an analogy between these
sets with the completely regular topological spaces, we call them completely
separated sets. Although the notion of an inequality induced by real-valued
functions is implicitly used by Bishop [3], p. 66, in his definition of a
complemented subset, an elaborate study of sets equipped with such an
inequality is missing. Ruitenburg’s work [45], in this journal, on
inequalities in $\mathrm{CM}$ is set-based.

The various distinctions revealed within $\mathrm{CM}$ are also reflected in
the various categories of sets that can be defined within $\mathrm{CM}$.
Besides the standard category $\mathrm{\mathbf{Set}}$ of sets $(X,=_{X})$ and
functions, we have the category SetIneq of sets with an inequality (see
Definition 2.1) and strongly extensional functions as arrows (see Definition
3.1). This category is the “universe” of Bishop-Cheng measure theory
$(\mathrm{BCMT})$, introduced in [4] and extended significantly in [5]. In
[37] we also introduce the category of strong sets SetStrong, a subcategory of
SetIneq, where the inequalities considered are equivalent to the strong
negation of the corresponding equalities, a positive and strong counterpart to
the standard weak negation. In the category SetComplSep of sets completely
separated by real-valued functions on them (see Definition 4.1), a subcategory
of SetIneq, the given inequalities and equalities are equivalent to ones
induced by a given set of real-valued functions. The importance of these
inequalities lies in the complete avoidance of negation in their definition
and in the proof of their basic properties. The category SetComplSep is the
‘universe” of Bishop measure theory222For the relation between $\mathrm{BMT}$
and $\mathrm{BCMT}$ see [33, 42, 43].$(\mathrm{BMT})$, developed in [3].

We work within Bishop Set Theory $(\mathrm{BST})$, an informal, constructive
theory of totalities and assignment routines, elaborated in [29, 33, 34, 35],
that serves as a “completion” of Bishop’s original theory of sets in [3, 5].
$\mathrm{BST}$ highlights fundamental notions that were suppressed by Bishop
in his account of the set theory underlying Bishop-style constructive
mathematics $(\mathrm{BISH})$, and serves as an intermediate step between
Bishop’s informal theory of sets and an adequate and faithful formalisation of
$\mathrm{BISH}$, in Feferman’s sense [11]. To assure faithfulness, we use
concepts or principles that appear, explicitly or implicitly, in
$\mathrm{BISH}$. The features of $\mathrm{BST}$ in [33] that somehow
“complete” Bishop’s original theory of sets are: the explicit use of an open-
ended universe $\mathbb{V}_{0}$ of predicative sets, a clear distinction
between sets and proper classes, such as $\mathbb{V}_{0}$, the explicit use of
dependent operations, and the elaboration of the theory of set-indexed
families of sets. Similarly to Martin-Löf Type Theory $(\mathrm{MLTT})$ (see
for example [15, 16]), $\mathrm{BST}$ behaves like a high-level programming
language333The type-theoretic interpretation of Bishop’s set theory into the
theory of setoids (see especially the work of Palmgren [18]-[23]) has become
nowadays the standard way to understand Bishop sets. For an analysis of the
relation between intensional $\mathrm{MLTT}$ and Bishop’s theory of sets see
[33], Chapter 1. Other formal systems for $\mathrm{BISH}$ are Myhill’s
Constructive Set Theory $(\mathrm{CST})$, introduced in [17], and Aczel’s
system $\mathrm{CZF}$ (see [1]). Palmgren’s work [20] and Coquand’s work [8]
are categorical approaches to Bishop sets..

We structure this paper as follows:

  * •

In section 2 we introduce the category SetIneq of sets with an inequality and
strongly extensional functions, and we define the Sigma-and the Pi-set of a
family of sets with an inequality over an index-set with an inequality.

  * •

In section 3 we define the canonical equality $=_{(X,F)}$ and inequality
$\neq_{(X,F)}$ induced on a set $(X,=_{X})$ by an extensional subset $F$ of
the real-valued functions $\mathbb{F}(X)$ on $X$. The extensionality and the
tightness of the inequality $\neq_{(X,F)}$ avoid completely the use of
negation. Basic properties of these inequalities are shown.

  * •

In section 4 we introduce the category SetComplSep of completely separated
sets, a full subcategory of SetIneq, and the category SetAffine of affine
sets, a subcategory of SetComplSep with affine arrows only. We define the
notion of a family of completely separated sets over an index-completely
separated set444All notions of families of sets defined here are not studied
in [33]., we describe its corresponding Pi-set, and we provide a sufficient
condition, in order to get a restricted form of a Sigma-set for it
(Proposition 4.6). By introducing the notion of a global family of completely
separated sets over an index-completely separated set, we manage to describe
its Sigma-set as a completely separated set, and to generalise the notion of a
strongly extensional function to dependent functions. The second projection of
the Sigma-set of such a global family is shown to be a strongly extensional
dependent function (Corollary 4.10(ii)).

  * •

In section 5 we define the free completely separated set $\varepsilon\bm{X}$
on a given set $(X,=_{X})$, we prove its universal property, and we show that
the functor
$\textnormal{{Free}}\colon\mathrm{\mathbf{Set}}\to\textnormal{{SetComplSep}}$
is left adjoint to the corresponding forgetful functor
$\textnormal{{Frg}}\colon\textnormal{{SetComplSep}}\to\mathrm{\mathbf{Set}}$.
Theorem 5.2 corresponds to the type-theoretic fact that the setoid
$(X,=_{X})$, where $=_{X}$ is the equality type family on the type $X$ in
intensional $\mathrm{MLTT}$, is the free setoid on the type $X$.

  * •

In section 6 we prove a purely set-theoretic version of the Stone-Čech theorem
in classical topology, according to which, to any topological space
corresponds a completely regular one such that the two spaces have isomorphic
rings of continuous, real-valued functions, and the corresponding functor is a
reflector. Replacing topological spaces with function spaces, that is triplets
$(X,=_{X};F)$ as above, and completely regular spaces with completely
separated sets, we correspond to any function space a completely separated set
with the same carrier set and (separating) set of functions (Theorem 6.2). The
corresponding functor
$\rho\colon\textnormal{{FunSpace}}\to\textnormal{{SetAffine}}$ is shown to be
a reflector, hence left adjoint to the corresponding embedding functor
$\textnormal{{Emb}}\colon\textnormal{{SetAffine}}\to\textnormal{{FunSpace}}$.
Moreover, Emb is also left adjoint to $\rho$ (Proposition 6.3).

  * •

In section 7 we prove a purely set-theoretic version of the Tychonoff
embedding theorem in classical topology, according to which, a $T_{1}$
topological space is completely regular if and only if it is topologically
embedded into a product of $[0,1]$. According to Theorem 7.5, if $(X,=_{X};F)$
is a function space, and if the induced inequality $\neq_{(X,F)}$ on $X$ is
tight, then there is an affine embedding of the completely separated set
$(X,=_{X},\neq_{(X,F)};F)$ into the completely separated set $\bm{R}^{F}$.
Conversely, if
$e\colon(X,=_{X};F)\to({\mathbb{R}}^{F},=_{{\mathbb{R}}^{F}};\bigotimes_{f\in
F}\\{\mathrm{id}_{{\mathbb{R}}}\\})$ is an affine embedding in FunSpace, the
induced inequality $\neq_{(X,F)}$ on $X$ is tight. The latter result provides
a criterion for the generation of a completely separated set from a given
function space.

For all notions and results from $\mathrm{BST}$ that are used here without
explanation or proof, we refer to [33]. For all categorical notions and facts
that are used here without explanation or proof, we refer to [2]. A
formulation of category theory within $\mathrm{BST}$ is presented in [40].

##  2 Sets with an inequality

In this section we introduce the category SetIneq of sets with an inequality.
We use a terminology on inequalities that is closer to [14], rather than to
[5]. In [5], p. 72, an inequality is what we call here an apartness relation.
In [47], p. 31, an inequality is considered to be always symmetric. As the
canonical inequality defined though strong negation in [37] is not in general
symmetric, an abstract inequality here is a relation on a set that contradicts
its given equality. In $\mathrm{BST}$ falsum is defined as the formula
$\bot:=0=_{{\mathbb{N}}}1$.

######  Definition 2.1.

If $(X,=_{X})$ is a set, and let the following formulas with respect to a
relation $x\neq_{X}y:$
$(\textnormal{{Ineq}}_{1})\ \forall_{x,y\in X}\big{(}x=_{X}y\ \&\
x\neq_{X}y\Rightarrow\bot\big{)}$,
$(\textnormal{{Ineq}}_{2})\ \forall_{x,x{{}^{\prime}},y,y{{}^{\prime}}\in
X}\big{(}x=_{X}x{{}^{\prime}}\ \&\ y=_{X}y{{}^{\prime}}\ \&\
x\neq_{X}y\Rightarrow x{{}^{\prime}}\neq_{X}y{{}^{\prime}}\big{)}$,
$(\textnormal{{Ineq}}_{3})\ \forall_{x,y\in
X}\big{(}\neg(x\neq_{X}y)\Rightarrow x=_{X}y\big{)}$,
$(\textnormal{{Ineq}}_{4})\forall_{x,y\in X}\big{(}x\neq_{X}y\Rightarrow
y\neq_{X}x\big{)}$,
$(\textnormal{{Ineq}}_{5})\ \forall_{x,y\in
X}\big{(}x\neq_{X}y\Rightarrow\forall_{z\in X}(z\neq_{X}x\ \vee\
z\neq_{X}y)\big{)}$,
$(\textnormal{{Ineq}}_{6})\ \forall_{x,y\in X}\big{(}x=_{X}y\vee
x\neq_{X}y\big{)}$.
If $\textnormal{{Ineq}}_{1}$ is satisfied, we call $\neq_{X}$ an inequality on
$X$, and the structure $\bm{X}:=(X,=_{X},\neq_{X})$ a set with an inequality.
We also write $|\bm{X}|:=X$. If $(\textnormal{{Ineq}}_{6})$ is satisfied, then
$\bm{X}$ is called discrete. An inequality is called extensional, if
$(\textnormal{{Ineq}}_{2})$ holds, and it is called tight, if
$(\textnormal{{Ineq}}_{3})$ is satisfied. An inequality satisfying
$(\textnormal{{Ineq}}_{4})$ and $(\textnormal{{Ineq}}_{5})$ is called an
apartness relation on $X$. If $\bm{Y}:=(Y,=_{Y},\neq_{Y})$ is a set with an
inequality, a function555If $(X,=_{X})$ and $(Y,=_{Y})$ are sets, an
assignment routine $f\colon X\rightsquigarrow Y$ is a function, if it
preserves the corresponding equalities. The notion of a (non-dependent)
assignment routine, that is of a routine that corresponds an element $f(x)$ of
$Y$ to each element $x$ of $X$, is primitive in $\mathrm{BST}$. $f\colon X\to
Y$ is strongly extensional, if,

$\forall_{x,y\in X}\big{(}f(x)\neq_{Y}f(y)\Rightarrow x\neq_{X}y\big{)}.$

Let $\mathbb{F}^{\neq}(\bm{X},\bm{Y})$ be the set666One needs the
extensionality of $\neq_{Y}$ to show that the strong extensionality of
$f\in\mathbb{F}(X,Y)$ is an extensional property on $\mathbb{F}(X,Y)$, and
define then $\mathbb{F}^{\neq}(\bm{X},\bm{Y})$ using the separation scheme. As
$(\textnormal{{Ineq}}_{2})$ is not considered here part of the definition of
an inequality, we introduce $\mathbb{F}^{\neq}(\bm{X},\bm{Y})$ independently
from $\mathbb{F}(X,Y)$. of strongly extensional functions from $\bm{X}$ to
$\bm{Y}$, equipped with the pointwise equality. Furthermore, let
$\mathbb{V}_{0}^{\neq}$ be the proper class of sets with an inequality,
equipped with the equality

$\bm{X}=_{\mathbb{V}_{0}^{\neq}}\bm{Y}:\Leftrightarrow\exists_{f\in\mathbb{F}^{\neq}(\bm{X},\bm{Y})}\exists_{g\in\mathbb{F}^{\neq}(\bm{Y},\bm{X})}\big{(}(f,g)\colon
X=_{\mathbb{V}_{0}}Y\big{)}.$

Let SetIneq be the category of sets with an inequality and strongly
extensional functions.

An equality is always extensional on $X\times X$. There are non-extensional
properties on a set, that is formulas $P(x)$, where $x$ is a variable of the
set $X$, such that $P(x)$ and $x=_{X}y$ do not imply $P(y)$. For example, let
$n\in{\mathbb{N}}$, $q\in\mathbb{Q}$ and $P_{q}(x)$, where $x$ is a variable
of set ${\mathbb{R}}$, defined by $P_{q}(x):=x_{n}=_{\mathbb{Q}}q.$ If
$y\in{\mathbb{R}}$ such that $y=_{{\mathbb{R}}}x$, then it is not necessary
that $y_{n}=_{\mathbb{Q}}q$, if $x_{n}=_{\mathbb{Q}}q$. It is not easy to give
examples of non strongly extensional functions, although we cannot accept in
$\mathrm{BISH}$ that all functions are strongly extensional. For example, the
strong extensionality of all functions from a metric space to itself is
equivalent to Markov’s principle (see [10], p. 40). Even to show that a
constant function between sets with an inequality is strongly extensional, one
needs intuitionistic, and not minimal, logic.

######  Remark 2.2.

An apartness relation on a set $(X,=_{X})$ is an extensional inequality.

###### Proof.

Let $x,y\in X$ with $x\neq_{X}y$, and $x{{}^{\prime}},y{{}^{\prime}}\in X$
with $x{{}^{\prime}}=_{X}x$ and $y{{}^{\prime}}=_{X}y$. By
$(\textnormal{{Ineq}}_{5})$ we get $x{{}^{\prime}}\neq_{X}x$, which is
excluded from $(\textnormal{{Ineq}}_{1})$, or $x{{}^{\prime}}\neq_{X}y$, which
has to be the case. Hence, $y{{}^{\prime}}\neq_{X}x{{}^{\prime}}$, or
$y{{}^{\prime}}\neq_{X}y$. Since the latter is excluded similarly, we get
$y{{}^{\prime}}\neq_{X}x{{}^{\prime}}$, hence by $(\textnormal{{Ineq}}_{4})$
we get $x{{}^{\prime}}\neq_{X}y{{}^{\prime}}$. ∎

For the canonical equalities of all sets mentioned here we refer to [33],
Chapter 2, and to [5].

######  Definition 2.3.

Let $\bm{X}:=(X,=_{X},\neq_{X})$ and $\bm{Y}:=(Y,=_{Y},\neq_{Y})$ be in
SetIneq, and let $\big{(}A,i_{A}\big{)}\subseteq X$. The canonical
inequalities on the product $X\times Y$, the function space $\mathbb{F}(X,Y)$
and $A$ are given, respectively, by

$(x,y)\neq_{X\times Y}(x{{}^{\prime}},y{{}^{\prime}}):\Leftrightarrow
x\neq_{X}x{{}^{\prime}}\vee y\neq_{Y}y{{}^{\prime}},$
$f\neq_{\mathbb{F}(X,Y)}g:\Leftrightarrow\exists_{x\in
X}\big{[}f(x)\neq_{Y}g(x)\big{]},$ $a\neq_{A}a{{}^{\prime}}:\Leftrightarrow
i_{A}(a)\neq_{X}i_{A}(a{{}^{\prime}}).$

The canonical inequality on the set of reals ${\mathbb{R}}$ is given by
$a\neq_{{\mathbb{R}}}b:\Leftrightarrow|a-b|>0\Leftrightarrow a>b\vee a<b$,
which is a special case of the canonical inequality on a metric space $(Z,d)$,
given by $z\neq_{(Z,d)}z{{}^{\prime}}:\Leftrightarrow d(z,z{{}^{\prime}})>0$.
Let $\bm{R}:=({\mathbb{R}},=_{{\mathbb{R}}},\neq_{{\mathbb{R}}})$,
$\bm{Z}:=(Z,=_{(Z,d)},\neq_{(Z,d)})$, and
$\bm{N}:=({\mathbb{N}},=_{{\mathbb{N}}},\neq_{{\mathbb{N}}})$. If
$\mathbb{2}:=\\{x\in{\mathbb{N}}\mid x=_{{\mathbb{N}}}0\vee
x=_{{\mathbb{N}}}1\\}$, let
$\bm{2}:=(\mathbb{2},=_{\mathbb{2}},\neq_{\mathbb{2}})$, where the
$($in$)$equality on $\mathbb{2}$ is induced by the $($in$)$equality on
${\mathbb{N}}$.

The inequalities $a\neq_{{\mathbb{R}}}b$, $z\neq_{(Z,d)}z{{}^{\prime}}$,
$\neq_{{\mathbb{N}}}$ and $\neq_{\mathbb{2}}$ are tight apartness relations.
Clearly, the projections $\textnormal{{pr}}_{X},\textnormal{{pr}}_{Y}$
associated to $X\times Y$, and also, by definition, the embedding $i_{A}^{X}$
of a subset $A$ of $X$, are strongly extensional functions. The dependent
assignment routines described next are primitive objects in $\mathrm{BST}$.

######  Definition 2.4.

If $(I,=_{I})$ is a set and $\lambda_{0}\colon
I\rightsquigarrow\mathbb{V}_{0}$ is an assignment routine that corresponds to
each element $i\in I$ a set $\lambda_{0}(i)$, a dependent assignment routine
$\Theta$ assigns to every element $i\in I$ an element $\Theta_{i}$ of
$\lambda_{0}(i)$. We denote by $\mathcal{D}\mathcal{O}(I,\lambda_{0})$ the
totality of dependent assignment routines over $I$ and $\lambda_{0}$, which
becomes a set with an inequality, if we consider the following pointwise
equality and inequality

$\Theta=_{\mathcal{D}\mathcal{O}(I,\lambda_{0})}\Theta{{}^{\prime}}:\Leftrightarrow\forall_{i\in
I}\big{(}\Theta_{i}=_{\lambda_{0}(i)}\Theta{{}^{\prime}}_{i}\big{)},$
$\Theta\neq_{\mathcal{D}\mathcal{O}(I,\lambda_{0})}\Theta{{}^{\prime}}:\Leftrightarrow\exists_{i\in
I}\big{(}\Theta_{i}\neq_{\lambda_{0}(i)}\Theta{{}^{\prime}}_{i}\big{)},$

where for the latter we suppose that every $\lambda_{0}(i)$ is equipped with
an inequality $\neq_{\lambda_{0}(i)}$.

A family of sets indexed by some set $(I,=_{I})$ is an assignment routine
$\lambda_{0}:I\rightsquigarrow\mathbb{V}_{0}$ that behaves like a function,
that is if $i=_{I}j$, then $\lambda_{0}(i)=_{\mathbb{V}_{0}}\lambda_{0}(j)$. A
more explicit definition, which is due to Richman, is included in [5], p. 78
(Problem 2), which is made precise in [33] by highlighting the role of
dependent assignment routines in its formulation. In accordance to the second
attitude described in the Introduction, this is a proof-relevant definition
revealing the witnesses of the equality
$\lambda_{0}(i)=_{\mathbb{V}_{0}}\lambda_{0}(j)$. We define the notion of a
family of sets within SetIneq similarly.

######  Definition 2.5.

If $\bm{I}:=(I,=_{I},\neq_{I})$ is in SetIneq, let the diagonal $D(I)$ of $I$,
defined by

$D(I):=\\{(i,j)\in I\times I\mid i=_{I}j\\}.$

A family of sets with an inequality indexed by $\bm{I}$ is a pair
$\Lambda:=(\lambda_{0},\lambda_{1})$, where $\lambda_{0}\colon
I\rightsquigarrow\mathbb{V}_{0}^{\neq}$,

$\overline{\lambda}_{0}(i):=\big{(}\lambda_{0}(i),=_{\lambda_{0}(i)},\neq_{\lambda_{0}(i)}\big{)},$

for every $i\in I$, and $\lambda_{1}$, a modulus of function-likeness for
$\lambda_{0}$, is a dependent operation

$\lambda_{1}\colon\bigcurlywedge_{(i,j)\in
D(I)}\mathbb{F}^{\neq}\big{(}\lambda_{0}(i),\lambda_{0}(j)\big{)},\ \ \
\lambda_{1}(i,j)=:\lambda_{ij},\ \ \ (i,j)\in D(I),$

such that the transport maps $\lambda_{ij}$ of $\boldmath\Lambda$ satisfy the
following conditions:
(a) For every $i\in I$, we have that
$\lambda_{ii}=\mathrm{id}_{\lambda_{0}(i)}$.
(b) If $i=_{I}j$ and $j=_{I}k$, the following triangle commutes

$\lambda_{0}(j)$$\lambda_{0}(k).$$\lambda_{0}(i)$$\lambda_{jk}$$\lambda_{ij}$$\
\lambda_{ik}$

If $\bm{X},\bm{Y}$ are in SetIneq, the constant $\bm{I}$-family of sets
$\bm{X}$ is the pair $\bm{C}^{X}:=(\bm{\lambda}_{0}^{X},\lambda_{1}^{X})$,
where $\lambda_{0}(i):=X$, for every $i\in I$, and
$\lambda_{1}(i,j):=\mathrm{id}_{X}$, for every $(i,j)\in D(I)$. The
$\bm{2}$-family $\boldmath\Lambda^{\mathbb{2}}(\bm{X},\bm{Y})$ of $\bm{X}$ and
$\bm{Y}$ is defined by $\lambda_{0}(0):=\bm{X}$, $\lambda_{0}(1):=\bm{Y}$,
$\lambda_{00}:=\mathrm{id}_{X}$ and $\lambda_{11}:=\mathrm{id}_{Y}$.

If $i=_{I}j$, then
$(\lambda_{ij},\lambda_{ji})\colon\bm{\lambda}_{0}(i)=_{\mathbb{V}_{0}^{\neq}}\bm{\lambda}_{0}(j)$.
Next we describe the Sigma-set (or the exterior union, or the disjoint union)
and the Pi-set (or the set of dependent functions) of a given family of sets
with an inequality.

######  Definition 2.6.

Let $\boldmath\Lambda:=(\lambda_{0},\lambda_{1})$ be an $\bm{I}$-family of
sets with an inequality. Its Sigma-set

$\sum_{I}\Lambda:=\bigg{(}\sum_{i\in I}\lambda_{0}(i),=_{{\sum_{i\in
I}\lambda_{0}(i)}},\neq_{{\sum_{i\in
I}\lambda_{0}(i)}}\bigg{)}\in\textnormal{{SetIneq}}$

is defined by

$w\in\sum_{i\in I}\lambda_{0}(i):\Leftrightarrow\exists_{i\in
I}\exists_{x\in\lambda_{0}(i)}\big{(}w:=(i,x)\big{)},$ $(i,x)=_{{\sum_{i\in
I}\lambda_{0}(i)}}(j,y):\Leftrightarrow i=_{I}j\ \&\
\lambda_{ij}(x)=_{\lambda_{0}(j)}y,$ $(i,x)\neq_{{\sum_{i\in
I}\lambda_{0}(i)}}(j,y):\Leftrightarrow i\neq_{I}j\ \vee\ \big{(}i=_{I}j\ \&\
\lambda_{ij}(x)\neq_{\lambda_{0}(j)}y\big{)}.$

The Sigma-set of the $\bm{2}$-family $\Lambda^{\mathbb{2}}(\bm{X},\bm{Y})$ of
$\bm{X}$ and $\bm{Y}$ is their coproduct. The first projection on $\sum_{i\in
I}\lambda_{0}(i)$ is the $($non-dependent$)$ operation777The global projection
operations $\textnormal{{pr}}_{1}$ and $\textnormal{{pr}}_{2}$ are primitive
operations in $\mathrm{BST}$.

$\textnormal{{pr}}_{1}^{\boldmath\Lambda}\colon\sum_{i\in
I}\lambda_{0}(i)\rightsquigarrow I,\ \ \ \
\textnormal{{pr}}_{1}^{\boldmath\Lambda}(i,x):=\textnormal{{pr}}_{1}(i,x):=i,\
\ \ \ (i,x)\in\sum_{i\in I}\lambda_{0}(i).$

The second projection on $\sum_{i\in I}\lambda_{0}(i)$ is the dependent
operation

$\textnormal{{pr}}_{2}^{\boldmath\Lambda}\colon\bigcurlywedge_{(i,x)\in\sum_{i\in
I}\lambda_{0}(i)}\lambda_{0}(i),\ \ \ \
\textnormal{{pr}}_{2}^{\boldmath\Lambda}(i,x):=\textnormal{{pr}}_{2}(i,x):=x,\
\ \ \ (i,x)\in\sum_{i\in I}\lambda_{0}(i).$

We write $\textnormal{{pr}}_{1},\textnormal{{pr}}_{2}$, if $\boldmath\Lambda$
is clearly understood from the context. The Pi-set of $\boldmath\Lambda$

$\prod_{I}\Lambda:=\bigg{(}\prod_{i\in I}\lambda_{0}(i),=_{{\prod_{i\in
I}\lambda_{0}(i)}},\neq_{{\prod_{i\in
I}\lambda_{0}(i)}}\bigg{)}\in\textnormal{{SetIneq}}$

is defined by

$\Theta\in\prod_{i\in
I}\lambda_{0}(i):\Leftrightarrow\Theta\in\mathcal{D}\mathcal{O}(I,\lambda_{0})\
\&\ \forall_{(i,j)\in
D(I)}\big{(}\Theta_{j}=_{\lambda_{0}(j)}\lambda_{ij}(\Theta_{i})\big{)},$

and $=_{{\prod_{i\in I}\lambda_{0}(i)}}$ and $\neq_{{\prod_{i\in
I}\lambda_{0}(i)}}$ are the the canonical pointwise equality and inequality,
respectively, inherited from $\mathcal{D}\mathcal{O}(I,\lambda_{0})$. If
$\bm{X}$ is in SetIneq and $C^{\bm{X}}$ is the constant $\bm{I}$-family
$\bm{X}$, let

$\bm{X}^{\bm{I}}:=\bigg{(}X^{I}:=\prod_{i\in
I}X,=_{X^{I}},\neq_{X^{I}}\bigg{)}.$

Clearly, if $i=_{I}j$ and $\Theta\in\prod_{i\in I}\lambda_{0}(i)$, then
$(i,\Theta_{i})=_{{\sum_{i\in I}\lambda_{0}(i)}}(j,\Theta_{j})$. Although the
canonical inequality $=_{{\sum_{i\in I}\lambda_{0}(i)}}$ is an inequality on
$\big{(}\sum_{i\in I}\lambda_{0}(i),\neq_{{\sum_{i\in
I}\lambda_{0}(i)}}\big{)}$, with respect to which
$\textnormal{{pr}}_{1}^{\boldmath\Lambda}$ is a strongly extensional function,
we need extra assumptions to make it an apartness relation. The proof of the
next proposition makes heavy use of negation, something that we shall avoid in
the subsequent sections, where inequalities induced by functions will be
considered.

######  Proposition 2.7.

Let $\boldmath\Lambda:=(\lambda_{0},\lambda_{1})$ be an $\bm{I}$-family of
sets with an inequality. If $\bm{I}$ is discrete, and $\neq_{\lambda_{0}(i)}$
is an apartness relation on $\lambda_{0}(i)$, for every $i\in I$, then
$\neq_{{\sum_{i\in I}\lambda_{0}(i)}}$ is an apartness relation. If
$\bm{\lambda}_{0}(i)$ is discrete, for every $i\in I$, then $\sum_{I}\Lambda$
is discrete, and if $\neq_{I}$ is tight and $\neq_{\lambda_{0}(i)}$ is tight,
for every $i\in I$, then $\neq_{{\sum_{i\in I}\lambda_{0}(i)}}$ is tight.

###### Proof.

The condition $(\textnormal{{Ineq}}_{1})$ of Definition 2.1 is trivially
satisfied. To show condition $(\textnormal{{Ineq}}_{4})$, we suppose first
that $i\neq_{I}j$, hence by the corresponding condition of $\neq_{I}$ we get
$(j,y)\neq_{{\sum_{i\in I}\lambda_{0}(i)}}(i,x)$. If $i=_{I}j\ \&\
\lambda_{ij}(x)\neq_{\lambda_{0}(j)}y$, we show that
$\lambda_{ji}(y)\neq_{\lambda_{0}(i)}x$. By the extensionality of
$\neq_{\lambda_{0}(j)}$ (Remark 2.2) the inequality
$\lambda_{ij}(x)\neq_{\lambda_{0}(j)}y$ implies the inequality
$\lambda_{ij}(x)\neq_{\lambda_{0}(j)}\lambda_{ij}\big{(}\lambda_{ji}(y)\big{)}$,
and since $\lambda_{ij}$ is strongly extensional, we get
$x\neq_{\lambda_{0}(i)}\lambda_{ji}(y)$. To show condition
$(\textnormal{{Ineq}}_{5})$, let $(i,x)\neq_{{\sum_{i\in
I}\lambda_{0}(i)}}(j,y)$, and let $(k,z)\in\sum_{i\in I}\lambda_{0}(i)$. If
$i\neq_{I}j$, then by condition $(\textnormal{{Ineq}}_{5})$ of $\neq_{I}$ we
get $k\neq_{I}i$, or $k\neq_{I}j$, hence $(k,z)\neq_{{\sum_{i\in
I}\lambda_{0}(i)}}(i,x)$, or $(k,z)\neq_{{\sum_{i\in I}\lambda_{0}(i)}}(j,y)$.
Suppose next $i=_{I}j\ \&\ \lambda_{ij}(x)\neq_{\lambda_{0}(j)}y$. As $\bm{I}$
is discrete, $k\neq_{I}i$, or $k=_{I}i=_{I}j$. If $k\neq_{I}i$, then what we
want to show follows immediately. If $k=_{I}i=_{I}j$, then by the
extensionality of $\neq_{\lambda_{0}(j)}$ and the strong extensionality of the
transport map $\lambda_{kj}$ we have that

$\lambda_{ij}(x)\neq_{\lambda_{0}(j)}y\Rightarrow\lambda_{kj}\big{(}\lambda_{ik}(x)\big{)}\neq_{\lambda_{0}(j)}\lambda_{kj}\big{(}\lambda_{jk}(y)\big{)}\Rightarrow\lambda_{ik}(x)\neq_{\lambda_{0}(k)}\lambda_{jk}(y).$

Hence, by condition $(\textnormal{{Ineq}}_{5})$ of $\neq_{\lambda_{0}(k)}$ we
get $\lambda_{ik}(x)\neq_{\lambda_{0}(k)}z$, or
$\lambda_{jk}(y)\neq_{\lambda_{0}(k)}z$, hence $(i,x)\neq_{{\sum_{i\in
I}\lambda_{0}(i)}}(k,z)$, or $(j,y)\neq_{{\sum_{i\in I}\lambda_{0}(i)}}(k,z)$.
Let $\overline{\lambda}_{0}(i)$ be discrete, for every $i\in I$. We show that
$(i,x)=_{{\sum_{i\in I}\lambda_{0}(i)}}(j,y)$, namely $i=_{I}j$ and
$\lambda_{ij}(x)=_{\lambda_{0}(i)}y$, or $(i,x)\neq_{{\sum_{i\in
I}\lambda_{0}(i)}}(j,y)$, that is $i\neq_{I}j$ or $i=_{I}j\ \&\
\lambda_{ij}(x)\neq_{\lambda_{0}(j)}y$. As $\bm{I}$ is discrete, $i=_{I}j$, or
$i\neq_{I}j$. In the first case, and since $\overline{\lambda}_{0}(j)$ is
discrete, we get $\lambda_{ij}(x)=_{\lambda_{0}(j)}y$ or
$\lambda_{ij}(x)\neq_{\lambda_{0}(j)}y$, and what we want follows immediately.
If $i\neq_{I}j$, we get $(i,x)\neq_{{\sum_{i\in I}\lambda_{0}(i)}}(j,y)$.
Finally, we suppose that $\neq_{I}$ is tight and $\neq_{\lambda_{0}(i)}$ is
tight, for every $i\in I$. Let $\neg\big{[}(i,x)\neq_{{\sum_{i\in
I}\lambda_{0}(i)}}(j,y)\big{]}$, that is

$\big{[}i\neq_{I}j\ \vee\ \big{(}i=_{I}j\ \&\
\lambda_{ij}(x)\neq_{\lambda_{0}(j)}y\big{)}\big{]}\Rightarrow\bot.$

From this hypothesis we get the conjunction888Here we use the logical
implication
$\big{(}(\phi\vee\psi)\Rightarrow\bot\big{)}\Rightarrow[(\phi\Rightarrow\bot)\
\&\ (\psi\Rightarrow\bot)]$.

$\big{[}i\neq_{I}j\Rightarrow\bot\big{]}\ \ \&\ \ \big{[}\big{(}i=_{I}j\ \&\
\lambda_{ij}(x)\neq_{\lambda_{0}(j)}y\big{)}\Rightarrow\bot\big{]}.$

By the tightness of $\neq_{I}$ we get $i=_{I}j$. The formula $\big{(}i=_{I}j\
\&\ \lambda_{ij}(x)\neq_{\lambda_{0}(j)}y\big{)}\Rightarrow\bot$ trivially
implies
$(i=_{I}j)\Rightarrow\big{(}\lambda_{ij}(x)\neq_{\lambda_{0}(j)}y\Rightarrow\bot\big{)}$,
and as its premiss $i=_{I}j$ is derived by the tightness of $\neq_{I}$, we get
$\lambda_{ij}(x)\neq_{\lambda_{0}(j)}y\Rightarrow\bot$. Since
$\neq_{\lambda_{0}(i)}$ is tight, we conclude that
$\lambda_{ij}(x)=_{\lambda_{0}(j)}y$, hence $(i,x)=_{{\sum_{i\in
I}\lambda_{0}(i)}}(j,y)$. ∎

Notice that the above inequality on the Sigma-set of a family
$\boldmath\Lambda$ does not give the canonical inequality of the product when
the constant family is considered. This will be resolved in section 3 with the
use of global families of completely separated sets. An abstract inequality
induces a notion of disjoint subsets and a complemented subset is a pair of
disjoint subsets, that is a subset with a given “complement”. Complemented
subsets are first-class citizens of Bishop-Cheng measure theory in [4, 5], a
constructive version of Daniell’s approach to measure theory, and of Bishop
measure theory in [3] (see [30, 39, 42, 43]).

##  3 Equalities and inequalities induced by functions

A completely positive notion of inequality is implicitly used in the
definition of a complemented subset in [3], p. 66. This is the inequality
induced by a set of real-valued functions on a given set. This concept,
together with the corresponding notion of equality induced by such a set of
functions, are the starting point of our study. Unless otherwise stated, in
the rest of the paper $(X,=_{X}),(Y,=_{Y}),(I,=_{I})$ are sets and $F,G,K$ are
extensional subsets of $\mathbb{F}(X),\mathbb{F}(Y)$ and $\mathbb{F}(I)$,
respectively999That is there is an extensional property $P_{F}$ on
$\mathbb{F}(X)$ such that  $F:=\big{\\{}f\in\mathbb{F}(X)\mid
P_{F}(f)\big{\\}},$ where the extensionality of $P_{F}$ is the property
$f=_{\mathbb{F}(X)}g\ \&\ P_{F}(f)\Rightarrow P_{F}(g)$, for every
$f,g\in\mathbb{F}(X)$. The use of extensional subsets, instead of arbitrary
subsets given by their embeddings, is crucial to the definition of affine
arrows in Definition 4.1, as the expression $f\in F$, which is in principle a
judgment, in Martin-Löf’s sense, is replaced by the formula $P_{F}(f)$ (see
also [38])..

######  Definition 3.1.

Let $\bm{X}$ be in SetIneq. The canonical equality $x=_{(X,F)}x{{}^{\prime}}$
on $X$ induced by $F$ is defined by

$x=_{(X,F)}x{{}^{\prime}}:\Leftrightarrow\forall_{f\in
F}\big{(}f(x)=_{{\mathbb{R}}}f(x{{}^{\prime}})\big{)},$

for every $x,x{{}^{\prime}}\in X$, and the canonical inequality
$x\neq_{(X,F)}x{{}^{\prime}}$ on $X$ induced by $F$ is defined by

$x\neq_{(X,F)}x{{}^{\prime}}:\Leftrightarrow\exists_{f\in
F}\big{(}f(x)\neq_{{\mathbb{R}}}f(x{{}^{\prime}})\big{)},$

for every $x,x{{}^{\prime}}\in X$. We write $f\colon
x\neq_{(X,F)}x{{}^{\prime}}$ to denote that $f\in F$ witnesses the inequality
$x\neq_{(X,F)}x{{}^{\prime}}$. The induced inequality
$x\neq_{(X,F)}x{{}^{\prime}}$ is equal to the given inequality $\neq_{X}$ of
$X$, if

$x\neq_{X}x{{}^{\prime}}\Leftrightarrow x\neq_{(X,F)}x{{}^{\prime}},$

for every $x,x{{}^{\prime}}\in X$. The inequality $\neq_{(X,F)}$ is called
tight, if,

$x=_{(X,F)}x{{}^{\prime}}\Rightarrow x=_{X}x{{}^{\prime}},$

for every $x,x{{}^{\prime}}\in X$, and in this case we call $F$ a separating
set of functions on $X$, or we say that $F$ separates the points of $X$. If
$\bm{Y}$ in SetIneq, and $\Phi$ is an extensional subset of $\mathbb{F}(X,Y)$,
the canonical $($in$)$equalities $(\neq_{(X,\Phi)})=_{(X,\Phi)}$ on $X$
induced by $\Phi$, and the tightness of $\neq_{(X,\Phi)}$ are defined in a
similar way.

######  Remark 3.2.

Let $(X,=_{X},\neq_{X})$ be a set with an inequality.
(i) For every $x,x{{}^{\prime}}\in X$ we have that
$x=_{X}x{{}^{\prime}}\Rightarrow x=_{(X,F)}x{{}^{\prime}}$.
(ii) If $F$ separates the points of $X$, the equality $=_{X}$ is equal to the
induced equality $=_{(X,F)}$ on $X$.
(iii) The inequality $\neq_{(X,F)}$ is tight with respect to the equality
$=_{(X,F)}$ on $X$.
(iv) The canonical inequality $x\neq_{(X,F)}x{{}^{\prime}}$ on $X$ induced by
$F$ is an apartness relation.
(v) If $\neq_{X}$ is equal to $\neq_{(X,F)}$, then $\neq_{X}$ is an apartness
relation.
(vi) $\neq_{(X,F)}$ is tight, according to Definition 3.1, if and only if it
is tight according to Definition 2.1.
(vii) If each $f\in F$ is strongly extensional, then
$x\neq_{(X,F)}x{{}^{\prime}}\Rightarrow x\neq_{X}x{{}^{\prime}}$, for every
$x,x{{}^{\prime}}\in X$.

###### Proof.

Cases (i)-(iii) are trivial, and (v) follows (iv). The proof of (iv) relies on
the fact that the canonical inequality $\neq_{{\mathbb{R}}}$ is an apartness
relation. For the proof of (vi), suppose that
$x=_{(X,F)}x{{}^{\prime}}\Rightarrow x=_{X}x{{}^{\prime}}$, and let
$\neg(x\neq_{(X,F)}x{{}^{\prime}})$. Then $x=_{(X,F)}x{{}^{\prime}}$, using
the tightness of $\neq_{{\mathbb{R}}}$: if $f\in F$ with
$f(x)\neq_{{\mathbb{R}}}f(x{{}^{\prime}})$, then by our hypothesis we get a
contradiction, hence
$\neg(\big{(}f(x)\neq_{{\mathbb{R}}}f(x{{}^{\prime}})\big{)}$. By the
tightness of $\neq_{{\mathbb{R}}}$ we get
$f(x)=_{{\mathbb{R}}}f(x{{}^{\prime}})$, and we get the required equality
$x=_{X}x{{}^{\prime}}$. For the converse implication, let
$\neg(x\neq_{(X,F)}x{{}^{\prime}})\Rightarrow x=_{X}x{{}^{\prime}}$, and
$x=_{(X,F)}x{{}^{\prime}}$. To show $x=_{X}x{{}^{\prime}}$, it suffices to
show $\neg(x\neq_{(X,F)}x{{}^{\prime}})$. Clearly, the hypothesis
$x\neq_{(X,F)}x{{}^{\prime}}$ together with the assumption
$x=_{(X,F)}x{{}^{\prime}}$ give the required contradiction. The proof of case
(vii) is immediate. ∎

By Remark 3.2(i), the given equality $x=_{X}x{{}^{\prime}}$ is “smaller” than
every induced equality $x=_{(X,F)}x{{}^{\prime}}$. The inequality
$\neq_{(X,F)}$ is an inequality, but no negation of some sort is used in its
definition, and the proof of its extensionality avoids negation, as it relies
on the extensionality of $\neq_{{\mathbb{R}}}$. By its extensionality,
$\neq_{(X,F)}$ provides a fully positive definition of the extensional empty
subset of $X$ induced by $F$, namely

$/{}\Box_{(X,F)}:=\big{\\{}x\in X\mid x\neq_{(X,F)}x\big{\\}}.$

With the help of the extensional empty subset a positive definition of the
property “a subset is empty”, defined negatively as “it is not inhabited” in
[7], p. 8, is possible. Following [42], if $(A,i_{A})\subseteq X$, we call $A$
empty, if $A\subseteq/{}\Box_{(X,F)}$ in $\mathcal{P}(X)$. Similarly, the
tightness of $\neq_{(X,F)}$ is formulated positively. Notice that the
contrapositive of tightness,
$\neg(x=_{X}x{{}^{\prime}})\Rightarrow\exists_{f\in
F}\big{(}f(x)\neq_{{\mathbb{R}}}f(x{{}^{\prime}})\big{)}$, is the standard,
classical property of separation of points $x,x{{}^{\prime}}\in X$ from $F$.
If $F$ is a Bishop topology of functions (see [24, 31, 34]), then
$x=_{(X,F)}x{{}^{\prime}}$ and $x\neq_{(X,F)}x{{}^{\prime}}$ are the canonical
equality and inequality of a Bishop space, respectively. The inequality
$a\neq_{{\mathbb{R}}}b$ is equal to
$\neq_{({\mathbb{R}},\mathrm{Bic}({\mathbb{R}}))}$, where
$\mathrm{Bic}({\mathbb{R}})$ is the topology of Bishop-continuous functions of
type ${\mathbb{R}}\to{\mathbb{R}}$ (see [24], Proposition 5.1.2, where even
pointwise continuous functions are shown to separate the reals). But we can go
even further, noticing that the following extensional subset of
$\mathbb{F}({\mathbb{R}})$

$\\{\mathrm{id}_{{\mathbb{R}}}\\}:=\big{\\{}f\in\mathbb{F}({\mathbb{R}})\mid
f=_{\mathbb{F}({\mathbb{R}})}\mathrm{id}_{{\mathbb{R}}}\big{\\}}$

separates the points of ${\mathbb{R}}$. If $(Z,d)$ is a metric space, let the
set

$U_{0}(Z):=\\{d_{z}\in\mathbb{F}(Z)\mid z\in Z\\},$

where $d_{z}(z{{}^{\prime}}):=d(z,z{{}^{\prime}})$, for every
$z{{}^{\prime}}\in Z$. Then $z\neq_{(Z,d)}z{{}^{\prime}}\Leftrightarrow
z\neq_{U_{0}(Z)}z{{}^{\prime}}$, for every $z,z{{}^{\prime}}\in Z$. The family
$\mathrm{Const}(X)$ of constant real-valued functions on $X$ is not
separating, in general. The following remark is straightforward to show.

######  Remark 3.3.

Let $(X,=_{X},\neq_{X})$, $F,F{{}^{\prime}}$ extensional subsets of
$\mathbb{F}(X)$ with $F\subseteq F{{}^{\prime}}$, and $x,x{{}^{\prime}}\in X$.
(i) $x=_{(X,F{{}^{\prime}})}x{{}^{\prime}}\Rightarrow
x=_{(X,F)}x{{}^{\prime}}$.
(ii) $x\neq_{(X,F)}x{{}^{\prime}}\Rightarrow
x\neq_{(X,F{{}^{\prime}})}x{{}^{\prime}}$.
(iii) If $\neq_{(X,F)}$ is tight, then $\neq_{(X,F{{}^{\prime}})}$ is tight.
(iv) $/{}\Box_{(X,F)}\subseteq/{}\Box_{(X,F{{}^{\prime}})}$.

Hence, $=_{(X,\mathbb{F}(X))}$ is the “smallest” equality on $X$ induced by
real-valued functions on $(X,=_{X})$, and $\neq_{(X,\mathbb{F}(X))}$ is the
largest inequality on $X$ induced by such functions.

##  4 Sets completely separated by functions

Next we introduce the category SetComplSep of sets completely separated by
functions. Roughly speaking, a set with an inequality $(X,=_{X},\neq_{X})$ is
completely separated, if there is an extensional subset $F$ of $\mathbb{F}(X)$
such that $=_{X}$ and $\neq_{X}$ “are” the ones induced by $F$. Consequently,
$\neq_{X}$ is a tight apartness relation, and this fact is formulated in a
completely positive, negation-free framework. In order to avoid quantification
over the powerset of $\mathbb{F}(X)$, which is a proper class, we take $F$ to
be part of the defining data in Definition 4.1101010In [42] an f-inequality
$\neq_{X}$ was defined impredicatively by the existence of an extensional
subset $F$ of $\mathbb{F}(X)$, such that $\neq_{X}$ is equivalent to
$\neq_{(X,F)}$..

######  Definition 4.1.

A completely separated set is a structure $(\bm{X};F)$, where
$\bm{X}:=(X,=_{X},\neq_{X})$ is in SetIneq and $F$ is an extensional subset of
$\mathbb{F}(X)$, such that $\neq_{X}$ is equal to $\neq_{(X,F)}$ and
$\neq_{(X,F)}$ is tight111111Hence, $=_{X}$ is also equal to the induced
equality $=_{(X,F)}$ on $X$. Moreover, $\neq_{X}$ is tight, but as the
tightness of $\neq_{X}$ is negativistic, we prefer the positive formulation of
the tightness of $\neq_{(X,F)}$ in the definition of a completely separated
set.. We call a function $h\colon(\bm{X};F)\to(\bm{Y};G)$ affine, or an affine
arrow, if $g\circ h\in F$, for every $g\in G$

$X$$Y$${\mathbb{R}}$,$h$$F\ni g\circ h\ $$g\in G$

that is $P_{F}(g\circ h)$, for every $g\in\mathbb{F}(Y)$ such that $P_{G}(g)$.
Let $\mathbb{V}_{0}^{\textnormal{{f}}}$ be the proper class of completely
separated sets, equipped with the equality of $\mathbb{V}_{0}^{\neq}$, and let
SetComplSep be the full subcategory of SetIneq of completely separated sets.
The category of affine sets SetAffine is the subcategory of SetComplSep with
the same objects and only the affine arrows between them.

By the extensionality of $F$ we get the extensionality of
$Q(h):\Leftrightarrow\forall_{g\in G}\big{(}g\circ h\in F\big{)}$ on
$\mathbb{F}(X,Y)$, hence by separation we define the set of affine arrows from
$(\bm{X};F)$ to $(\bm{Y};G)$, that is

$\mathbb{Af}\big{(}(\bm{X};F),(\bm{Y};G)\big{)}:=\big{\\{}h\in\mathbb{F}(X,Y)\mid
Q(h)\big{\\}}.$

Following the previous section,
$\big{(}\bm{R};\\{\mathrm{id}_{{\mathbb{R}}}\\}\big{)}$ and
$\big{(}\bm{Z};U_{0}(Z)\big{)}$ are completely separated. Actually, if
$(\bm{X};F)$ is in SetComplSep, every element $f$ of $F$ is an affine arrow
from $(\bm{X};F)$ to $\big{(}\bm{R};\\{\mathrm{id}_{{\mathbb{R}}}\\}\big{)}$.
Clearly, an affine arrow between completely separated sets is a strongly
extensional function, or an arrow in SetComplSep. By Markov’s principle every
function from ${\mathbb{R}}$ to ${\mathbb{R}}$ is strongly extensional, but
not necessarily affine. Using intuitionisitic logic, and supposing that $F$
does not include the constant functions on $X$, a constant function from $X$
to $Y$ is strongly extensional, but not affine.

######  Proposition 4.2.

Let $(\bm{X};F):=(X,=_{X},\neq_{X};F)$ and $(\bm{Y};G):=(Y,=_{Y},\neq_{Y};G)$
be in SetComplSep, and let $(A,i_{A})\subseteq X$.
(i) The product $(\bm{X}\times\bm{Y};F\otimes G):=(X\times Y,=_{X\times
Y},\neq_{X}{\otimes}\neq_{Y};F\otimes G)$ is a completely separated set, where

$(x,y)\neq_{X}{\otimes}\neq_{Y}(x{{}^{\prime}},y{{}^{\prime}}):\Leftrightarrow
x\neq_{(X,F)}x{{}^{\prime}}\vee
y\neq_{(Y,G)}y{{}^{\prime}}\Leftrightarrow(x,y)\neq_{{(X\times Y,F\otimes
G)}}(x{{}^{\prime}},y{{}^{\prime}}),$ $F\otimes
G:=\\{f\circ\textnormal{{pr}}_{X}\mid f\in
F\\}\cup\\{g\circ\textnormal{{pr}}_{Y}\mid g\in G\\}.$

The projections $\textnormal{{pr}}_{X}\colon(\bm{X}\times\bm{Y};F\otimes
G)\to(\bm{X};F)$ and $\textnormal{{pr}}_{Y}\colon(\bm{X}\times\bm{Y};F\otimes
G)\to(\bm{Y};G)$ are affine arrows121212Hence, $(\bm{X}\times\bm{Y};F\otimes
G)$ is the product in SetAffine..
(ii) The function set
$\big{(}\mathbb{F}(X,Y),=_{\mathbb{F}(X,Y)},\neq_{\mathbb{F}(X,Y)};F\to
G\big{)}$ is a completely separated set, where

$h\neq_{\mathbb{F}(X,Y)}h{{}^{\prime}}:\Leftrightarrow\exists_{x\in
X}\big{(}h(x)\neq_{(Y,G)}h{{}^{\prime}}(x)\big{)}\Leftrightarrow
h\neq_{{(\mathbb{F}(X,Y),F\to G)}}h{{}^{\prime}},$ $F\to G:=\\{\phi_{x,g}\mid
x\in X\ \&\ g\in G\\},$ $\phi_{x,g}\colon\mathbb{F}(X,Y)\to{\mathbb{R}},\ \ \
\phi_{x,g}(h):=g(h(x)),\ \ \ h\in\mathbb{F}(X,Y).$

(iii) $\big{(}A,=_{A},\neq_{A};F\circ i_{A}\big{)}$ is completely separated,
where $a\neq_{A}a{{}^{\prime}}:\Leftrightarrow
i_{A}(a)\neq_{(X,F)}i_{A}(a{{}^{\prime}})\Leftrightarrow a\neq_{{F\circ
i_{A}}}a{{}^{\prime}},$

$F\circ i_{A}:=\\{f\circ i_{A}\mid f\in F\\},$

and $i_{A}\colon(A,=_{A},\neq_{A};F\circ i_{A})\to(X,=_{X},\neq_{X};F)$ is an
affine arrow.

###### Proof.

We show only (i) and (ii), as the proof of (iii) is immediate. For (i), if
$(x,y),(x{{}^{\prime}},y{{}^{\prime}})\in X\times Y$, then

$\displaystyle(x,y)\neq_{{(X\times Y,F\otimes
G)}}(x{{}^{\prime}},y{{}^{\prime}})$
$\displaystyle:\Leftrightarrow\exists_{h\in F\otimes
G}\big{(}h((x,y))\neq_{{\mathbb{R}}}h((x{{}^{\prime}},y{{}^{\prime}}))\big{)}$
$\displaystyle\Leftrightarrow\exists_{f\in
F}\big{(}(f\circ\textnormal{{pr}}_{X})((x,y))\neq_{{\mathbb{R}}}(f\circ\textnormal{{pr}}_{X})((x{{}^{\prime}},y{{}^{\prime}}))\big{)}\vee$
$\displaystyle\ \ \ \ \ \exists_{g\in
G}\big{(}(g\circ\textnormal{{pr}}_{Y})((x,y))\neq_{{\mathbb{R}}}(g\circ\textnormal{{pr}}_{Y})((x{{}^{\prime}},y{{}^{\prime}}))\big{)}$
$\displaystyle\Leftrightarrow:x\neq_{(X,F)}x{{}^{\prime}}\vee
y\neq_{(Y,G)}y{{}^{\prime}}.$

The tightness of $\neq_{X}{\otimes}\neq_{Y}$ follows from $(x,y)=_{{(X\times
Y,F\otimes G)}}(x{{}^{\prime}},y{{}^{\prime}})\Leftrightarrow
x=_{(X,F)}x{{}^{\prime}}\ \&\ y=_{(Y,G)}y{{}^{\prime}}$ and the tightness of
$\neq_{F}$ and $\neq_{G}$. The fact that the projections are affine arrows
follows immediately.
(ii) If $h,h{{}^{\prime}}\in\mathbb{F}(X,Y)$, we have that

$\displaystyle h\neq_{{(\mathbb{F}(X,Y),F\to G)}}h{{}^{\prime}}$
$\displaystyle:\Leftrightarrow\exists_{x\in X}\exists_{g\in
G}\big{(}\phi_{x,g}(h)\neq_{{\mathbb{R}}}\phi_{x,g}(h{{}^{\prime}})\big{)}$
$\displaystyle\Leftrightarrow\exists_{x\in X}\exists_{g\in
G}\big{(}g(h(x))\neq_{{\mathbb{R}}}g(h{{}^{\prime}}(x))\big{)}$
$\displaystyle\Leftrightarrow\exists_{x\in
X}\big{(}h(x)\neq_{(Y,G)}h{{}^{\prime}}(x)\big{)}$
$\displaystyle\Leftrightarrow:h\neq_{\mathbb{F}(X,Y)}h{{}^{\prime}}.$

As $\neq_{(Y,G)}$ is tight, we get

$\displaystyle\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\ \ \ \ \ \ \ \ \ \ \ \ \ \ h=_{{(\mathbb{F}(X,Y),F\to G)}}h{{}^{\prime}}$
$\displaystyle:\Leftrightarrow\forall_{x\in X}\forall_{g\in
G}\big{(}\phi_{x,g}(h)=_{{\mathbb{R}}}\phi_{x,g}(h{{}^{\prime}})\big{)}$
$\displaystyle\Leftrightarrow\forall_{x\in X}\forall_{g\in
G}\big{(}g(h(x))=_{{\mathbb{R}}}g(h{{}^{\prime}}(x))\big{)}$
$\displaystyle\Leftrightarrow\forall_{x\in
X}\big{(}h(x)=_{(Y,G)}h{{}^{\prime}}(x)\big{)}$
$\displaystyle\Rightarrow\forall_{x\in
X}\big{(}h(x)=_{Y}h{{}^{\prime}}(x)\big{)}$
$\displaystyle\Leftrightarrow:h=_{\mathbb{F}(X,Y)}h{{}^{\prime}}.\ \ \ \ \ \ \
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \qed$

Next we define a family of completely separated sets indexed by a completely
separated set $(\bm{I};K)$.

######  Definition 4.3.

If $(\bm{I};K)$ is in SetComplSep, a family of completely separated sets
indexed by $(\bm{I};K)$ is a structure
$\bm{S}:=(\lambda_{0},\lambda_{1};\phi_{0},\phi_{1})$, where
$(\lambda_{0},\lambda_{1})$ is an $\bm{I}$-family of sets with an inequality,
$\phi_{0}\colon I\rightsquigarrow\mathbb{V}_{0}$ with $\phi_{0}(i):=F_{i}$, an
extensional subset of $\mathbb{F}(\lambda_{0}(i))$, and

$\phi_{1}\colon\bigcurlywedge_{(i,j)\in
D(I)}\mathbb{F}\big{(}F_{i},F_{j}\big{)},\ \ \ \phi_{1}(i,j)=:\phi_{ij}\colon
F_{i}\to F_{j},\ \ \ (i,j)\in D(I),$

such that the following conditions hold:
(a) $x_{i}\neq_{\lambda_{0}(i)}x_{i}{{}^{\prime}}\Leftrightarrow
x_{i}\neq_{(\lambda_{0}(i),F_{i})}x_{i}{{}^{\prime}}$, for every
$x_{i},x_{i}{{}^{\prime}}\in\lambda_{0}(i)$ and $i\in I$.
(b) $x_{i}=_{(\lambda_{0}(i),F_{i})}x_{i}{{}^{\prime}}\Rightarrow
x_{i}=_{\lambda_{0}(i)}x_{i}{{}^{\prime}}$, for every
$x_{i},x_{i}{{}^{\prime}}\in\lambda_{0}(i)$ and $i\in I$.
(c) If $i=_{I}j$, then the following triangle commutes

$\lambda_{0}(j)$$\lambda_{0}(i)$${\mathbb{R}}$.$\lambda_{ji}$$F_{j}\ni\phi_{ij}(f_{i})\
\ $$f_{i}\in F_{i}$

We write $\big{(}\bm{\lambda}_{0}(i);F_{i}\big{)}$ in SetComplSep, for every
$i\in I$.

If $(\bm{X};F)$ and $(\bm{Y};G)$ are in SetComplSep, it is easy to define the
constant family $(\bm{X};F)$ over $(\bm{I};K)$ and the
$\big{(}\bm{2};\mathbb{F}(\mathbb{2})\big{)}$-family of $(\bm{X};F)$ and
$(\bm{Y};G)$.

######  Remark 4.4.

Let $\bm{S}:=(\lambda_{0},\lambda_{1};\phi_{0},\phi_{1})$ be a family of
completely separated sets over $(\bm{I};K)$.
(i) $\phi_{ij}$ is strongly extensional, for every $(i,j)\in D(I)$.
(ii) $\lambda_{ij}$ is an affine arrow, for every $(i,j)\in D(I)$.
(iii) The pair $(\phi_{0},\phi_{1})$ induces an $\bm{I}$-family of sets with
an inequality.
(iv) The pair $(\phi_{0},\phi_{1})$ induces an $(\bm{I};K)$-family of
completely separated sets.

###### Proof.

(i) If $f_{i},f_{i}{{}^{\prime}}\in F_{i}$, then we have that

$\displaystyle\phi_{ij}(f_{i})\neq_{F_{j}}\phi_{ij}(f_{i}{{}^{\prime}})$
$\displaystyle:\Leftrightarrow\exists_{y\in\lambda_{0}(j)}\big{(}[\phi_{ij}(f_{i})](y)\neq_{{\mathbb{R}}}[\phi_{ij}(f_{i}{{}^{\prime}})](y)\big{)}$
$\displaystyle\Leftrightarrow\exists_{y\in\lambda_{0}(j)}\big{(}f_{i}(\lambda_{ji}(y))\neq_{{\mathbb{R}}}f_{i}{{}^{\prime}}(\lambda_{ji}(y))\big{)}$
$\displaystyle\Rightarrow\exists_{x\in\lambda_{0}(i)}\big{(}f_{i}(x)\neq_{{\mathbb{R}}}f_{i}{{}^{\prime}}(x)\big{)}$
$\displaystyle\Leftrightarrow:f_{i}\neq_{F_{i}}f_{i}{{}^{\prime}}.$

(ii) It follows immediately by condition (c) in Definition 4.3.
(iii) Let
$\overline{\phi}_{0}(i):=\big{(}F_{i},=_{F_{1}},\neq_{F_{i}}\big{)}$, for
every $i\in I$. We use (i), and by condition (c) in Definition 4.3 we get
$\phi_{ii}(f_{i})=f_{i}\circ\lambda_{ii}=f_{i}$, for every $f_{i}\in F_{i}$.
We show the commutativity of the following triangle

$F_{j}$$F_{k},$$F_{i}$$\phi_{jk}$$\phi_{ij}$$\ \phi_{ik}$

with the commutativity of the corresponding triangle for
$(\lambda_{0},\lambda_{1})$ as follows:
$(\phi_{jk}\circ\phi_{ij})(f_{i})=(f_{i}\circ\lambda_{ji})\circ\lambda_{kj}$
$=f_{i}\circ(\lambda_{ji}\circ\lambda_{kj})=f_{i}\circ\lambda_{ki}=\phi_{ik}(f_{i})$.
(iv) Let the quadruple $\big{(}\bm{\phi}_{0},\phi_{1};\theta_{0},\theta_{1})$,
where $\theta_{0}(i):=\widehat{\lambda_{0}(i)}:=\\{\widehat{x}\mid
x\in\lambda_{0}(i)\\},$ and $\widehat{x}\colon F_{i}\to{\mathbb{R}}$ is given
by $\widehat{x}(f_{i}):=f_{i}(x)$, for every $x\in\lambda_{0}(i)$ and $i\in
I$. and $\theta_{ij}\colon\widehat{\lambda_{0}(i)}\to\widehat{\lambda_{0}(j)}$
is given by $\theta_{ij}\big{(}\widehat{x}\big{)}:=\widehat{\lambda_{ij}(x)}$,
for every $x\in\lambda_{0}(i)$ and $(i,j)\in D(I)$. It is now straightforward
to show conditions (a)–(c) of Definition 4.3. ∎

The Sigma-set and the Pi-set of an $(\bm{I};K)$-family $\bm{S}$ of completely
separated sets are defined as in Definition 2.6. According to the next
proposition, the Pi-set of such a family is in SetComplSep.

######  Proposition 4.5.

If $\bm{S}:=(\lambda_{0},\lambda_{1};\phi_{0},\phi_{1})$ is an
$(\bm{I};K)$-family of completely separated sets, then

$\prod_{I}\bm{S}:=\bigg{(}\prod_{i\in I}\lambda_{0}(i),=_{\prod_{i\in
I}\lambda_{0}(i)},\neq_{\prod_{i\in I}\lambda_{0}(i)}\ ;\ \bigotimes_{i\in
I}F_{i}\bigg{)}\in\textnormal{{SetComplSep}},$

where

$\bigotimes_{i\in
I}F_{i}:=\bigg{\\{}f_{i}\circ\textnormal{{pr}}_{i}^{\boldmath\Lambda}\mid
f_{i}\in F_{i},\ i\in I\bigg{\\}}.$

###### Proof.

Proceeding as in the proof of Proposition 4.2(i), we get

$\Theta\neq_{\prod_{i\in
I}\lambda_{0}(i)}\Theta{{}^{\prime}}:\Leftrightarrow\exists_{i\in
I}\big{(}\Theta_{i}\neq_{\lambda_{0}(i)}\Theta_{i}{{}^{\prime}}\big{)}\Leftrightarrow\Theta\neq_{\big{(}\prod_{i\in
I}\lambda_{0}(i),\bigotimes_{i\in I}F_{i}\big{)}}\Theta{{}^{\prime}}.\qed$

Similarly, the operation
$\textnormal{{pr}}_{i}^{\boldmath\Lambda}\colon\prod_{i\in
I}\lambda_{0}(i)\rightsquigarrow\lambda_{0}(i)$, defined by
$\Theta\mapsto\Theta_{i},$ is an affine arrow, for every $i\in I$. If
$(\bm{I};K)$ is discrete, and $\bm{S}$ is an $(\bm{I};K)$-family of completely
separated sets, then working as in the proof of Proposition 2.7 we get an
apartness relation on $\sum_{i\in I}\lambda_{0}(i)$, with respect to which
$\textnormal{{pr}}_{1}^{\boldmath\Lambda}$ is strongly extensional. Next we
examine whether this inequality is induced by a set of functions.

######  Proposition 4.6.

Let $(\bm{I};K)$ be discrete, and
$\bm{S}:=(\lambda_{0},\lambda_{1};\phi_{0},\phi_{1})$ an $(\bm{I};K)$-family
of completely separated sets. Let the following extensional subsets of
$\mathbb{F}\big{(}\sum_{i\in I}\lambda_{0}(i)\big{)}:$

$\widehat{K}:=\big{\\{}\widehat{k}\mid k\in K\big{\\}},$
$\widehat{k}\colon\sum_{i\in I}\lambda_{0}(i)\to{\mathbb{R}},\ \ \ \
\widehat{k}((i,x)):=k(i),\ \ \ \ (i,x)\in\sum_{i\in I}\lambda_{0}(i),$
$\widehat{H}:=\bigg{\\{}\widehat{\Phi}\mid\Phi\in\prod_{i\in
I}F_{i}\bigg{\\}},$ $\widehat{\Phi}\colon\sum_{i\in
I}\lambda_{0}(i)\to{\mathbb{R}},\ \ \ \ \widehat{\Phi}(i,x):=\Phi_{i}(x),\ \ \
\ (i,x)\in\sum_{i\in I}\lambda_{0}(i).$

(i) For every $(i,x),(j,y)\in\sum_{i\in I}\lambda_{0}(i)$, we have that

$(i,x)\neq_{{\widehat{K}\cup\widehat{H}}}(j,y)\Rightarrow(i,x)\neq_{{\sum_{i\in
I}\lambda_{0}(i)}}(j,y).$

(ii) If for every $j\in I$ and every $h\in F_{j}$ there is $\Phi\in\prod_{i\in
I}F_{i}$, such that $\Phi_{j}=_{\mathbb{F}(\lambda_{0}(j)}h$, then for every
$(i,x),(j,y)\in\sum_{i\in I}\lambda_{0}(i)$, we have that

$(i,x)\neq_{{\sum_{i\in
I}\lambda_{0}(i)}}(j,y)\Rightarrow(i,x)\neq_{{\widehat{K}\cup\widehat{H}}}(j,y).$

###### Proof.

(i) If there is $k\in K$ such that
$\widehat{k}((i,x)):=k(i)\neq_{{\mathbb{R}}}k(j)=:\widehat{k}((j,y))$, then
$i\neq_{K}j$, and the required inequality follows. Let $\Phi\in\prod_{i\in
I}F_{i}$ such that

$\widehat{\Phi}(i,x):=\Phi_{i}(x)\neq_{{\mathbb{R}}}\Phi_{j}(y)=:\widehat{\Phi}(j,y).$

If $i\neq_{K}j$, then we are reduced to the previous case. If $i=_{I}j$, then

$\Phi_{i}(x)=[\phi_{ji}(\Phi_{j})](x)=\Phi_{j}(\lambda_{ij}(x))\neq\Phi_{j}(y),$

hence $\lambda_{ij}(x)\neq_{\lambda_{0}(j)}y$, as by the definition of a
family of completely separated sets the elements of $F_{j}$, for every $j\in
I$, are strongly extensional functions. The required inequality follows then
immediately.
(ii) If $i\neq_{K}j$, the implication follows trivially. If $i=_{I}j$ and
$\lambda_{ij}(x)\neq_{\lambda_{0}(j)}y$, there is $h\in F_{j}$ such that
$h(\lambda_{ij}(x))\neq_{{\mathbb{R}}}h(y)$. Let $\Phi\in\prod_{i\in I}F_{i}$,
such that $\Phi_{j}=h$. As
$\Phi_{i}=\phi_{ji}(\Phi_{j})=\Phi_{j}\circ\lambda_{ij}$, we get

$\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\widehat{\Phi}(i,x):=\Phi_{i}(x)=_{{\mathbb{R}}}\Phi_{j}(\lambda_{ij}(x))=_{{\mathbb{R}}}h(\lambda_{ij}(x))\neq_{{\mathbb{R}}}h(y)=_{{\mathbb{R}}}\Phi_{j}(y)=:\widehat{\Phi}(j,y).\
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \qed$

By Proposition 4.6 to get that the Sigma-set of $\bm{S}$ is completely
separated, we need a discrete, completely separated index-set $(\bm{I};K)$,
and to suppose that for every $j\in I$, every element of $F_{j}$ is “extended”
to an element of $\prod_{i\in I}F_{i}$. To overcome these difficulties, we
introduce the notion of a global family of completely separated sets. In
contrast to Definition 2.5, where the transport maps $\lambda_{ij}$ are
defined on pairs $(i,j)$ with $i=_{I}j$, in a global family the transport maps
are defined on every pair $(i,j)$.

######  Definition 4.7.

If $\bm{I}$ is in SetIneq, a global $\bm{I}$-family of sets with an inequality
is a pair $\boldmath\Lambda^{*}:=(\lambda_{0},\lambda_{1}^{*})$, where
$\lambda_{0}\colon I\rightsquigarrow\mathbb{V}_{0}^{\neq}$, and

$\lambda_{1}^{*}\colon\bigcurlywedge_{(i,j)\in I\times
I}\mathbb{F}^{\neq}\big{(}\lambda_{0}(i),\lambda_{0}(j)\big{)},\ \ \
\lambda_{1}^{*}(i,j):=\lambda_{ij}^{*},\ \ \ (i,j)\in I\times I,$

such that the global transport maps $\lambda_{ij}^{*}$ of
$\boldmath\Lambda^{*}$ satisfy condition (a) of Definition 2.5 and condition
(b) of Definition 2.5, for every $i,j\in I$ with $i=_{I}j$, and every $k\in
I$. If $(\bm{I};K)$ is in SetComplSep, an $(\bm{I};K)$-family of completely
separated sets is a structure
$\bm{S}^{*}:=(\lambda_{0},\lambda_{1}^{*};\phi_{0},\phi_{1}^{*})$, where
$(\lambda_{0},\lambda_{1}^{*})$ is a global $\bm{I}$-family of sets with an
inequality, $\phi_{0}$ is as in Definition 4.3,

$\phi_{1}^{*}\colon\bigcurlywedge_{(i,j)\in I\times
I}\mathbb{F}\big{(}F_{i},F_{j}\big{)},\ \ \
\phi_{1}^{*}(i,j):=\phi_{ij}^{*}\colon F_{i}\to F_{j},\ \ \ (i,j)\in I\times
I,$

and the global maps $\phi_{ij}^{*}$ satisfy conditions (a, b) of Definition
4.3 and condition (c) of Definition 4.3, for every $i,j\in I$. The equality
and inequality of the Sigma-set of $\Lambda^{*}(S^{*})$ are given by

$(i,x)=_{{\sum_{i\in I}\lambda_{0}(i)}}(j,y):\Leftrightarrow i=_{I}j\ \&\
\lambda_{ij}^{*}(x)=_{\lambda_{0}(j)}y,$ $(i,x)\neq_{{\sum_{i\in
I}\lambda_{0}(i)}}(j,y):\Leftrightarrow i\neq_{(I,K)}j\ \vee\
\lambda_{ij}^{*}(x)\neq_{\lambda_{0}(j)}y.$

The Pi-set of $\Lambda^{*}(S^{*})$ is defined as in Definition 2.6.

The constant global $\bm{I}$-family of sets with an inequality $\bm{X}$ is
defined as the constant $\bm{I}$-family $\bm{X}$, with
$\lambda_{ij}^{*}:=\mathrm{id}_{X}$, for every $(i,j)\in I\times I$. If this
constant global family is considered, then the inequality of its Sigma-set is
reduced to the inequality of the product set. The constant global
$(\bm{I};K)$-family of completely separated sets $(\bm{X};F)$ is defined as
the constant $(\bm{I};K)$-family $(\bm{X};F)$, with
$\phi_{ij}^{*}:=\mathrm{id}_{F}$, for every $(i,j)\in I\times I$. To define
the global $\bm{2}$-family $\boldmath\Lambda^{\mathbb{2}}(\bm{X},\bm{Y})$ of
$\bm{X}$ and $\bm{Y}$, we add any two strongly extensional functions
$\lambda_{01}^{*}\colon X\to Y$ and $\lambda_{10}^{*}\colon Y\to X$, as the
following triangles trivially commute

$X$$Y$$X$$Y$$Y$$X$.$\lambda_{01}^{*}$$\mathrm{id}_{X}$$\
\lambda_{01}^{*}$$\lambda_{10}^{*}$$\mathrm{id}_{Y}$$\ \lambda_{10}^{*}$

To define the global $\big{(}\bm{2};\mathbb{F}(\mathbb{2})\big{)}$-family of
$(\bm{X};F)$ and $(\bm{Y};G)$, we also add maps $\phi_{01}^{*}\colon F\to G$
and $\phi_{10}^{*}\colon G\to F$, such that the following triangles commute

$X$$Y$${\mathbb{R}}$$Y$$X$${\mathbb{R}}$,$\lambda_{01}^{*}$$F\ni\phi_{10}^{*}(g)\
$$g\in G$$G\ni\phi_{01}^{*}(f)\ $$\lambda_{10}^{*}$$f\in F$

and moreover, $g\circ\lambda_{01}^{*}\in F$ and $f\circ\lambda_{10}^{*}\in G$,
for every $g\in G$ and $f\in F$, respectively. Next we show that the Sigma-set
of a global $(\bm{I};K)$-family of completely separated sets is also
completely separated.

######  Theorem 4.8.

Let $(\bm{I};K)$ be completely separated and let
$\bm{S}^{*}:=(\lambda_{0},\lambda_{1}^{*};\phi_{0},\phi_{1}^{*})$ be a global
$(\bm{I};K)$-family of completely separated sets. Let the extensional subsets
$\widehat{K}$ and $\widehat{H}$ of $\mathbb{F}\big{(}\sum_{i\in
I}\lambda_{0}(i)\big{)}$ that were defined in Proposition 4.6. If the Sigma-
set of $\boldmath\Lambda^{*}$ is equipped with the equality and inequality
given in Definition 4.7, then for every $(i,x),(j,y)\in\sum_{i\in
I}\lambda_{0}(i)$ we have that

$(i,x)\neq_{{\widehat{K}\cup\widehat{H}}}(j,y)\Leftrightarrow(i,x)\neq_{{\sum_{i\in
I}\lambda_{0}(i)}}(j,y),$

and hence

$\sum_{I}\bm{S}^{*}:=\bigg{(}\sum_{i\in I}\lambda_{0}(i),=_{\sum_{i\in
I}\lambda_{0}(i)},\neq_{\sum_{i\in I}\lambda_{0}(i)}\ ;\
\widehat{K}\cup\widehat{H}\bigg{)}\in\textnormal{{SetComplSep}}.$

###### Proof.

To show
$(i,x)\neq_{{\widehat{K}\cup\widehat{H}}}(j,y)\Rightarrow(i,x)\neq_{{\sum_{i\in
I}\lambda_{0}(i)}}(j,y)$, we work exactly as in the proof of Proposition
4.6(i). For the converse implication, we work as in the proof of Proposition
4.6(ii). It suffices to show that, if $h\in F_{j}$ with
$h(\lambda_{ij}^{*}(x))\neq_{{\mathbb{R}}}h(y)$, then there is
$\Phi^{h}\in\prod_{i\in I}F_{i}$ with $\Phi^{h}_{j}=h$. If $i\in I$, we define
$\Phi_{i}^{h}:=h\circ\lambda_{ij}^{*}$

$\lambda_{0}(i)$$\lambda_{0}(j)$${\mathbb{R}}$.$\lambda_{ij}^{*}$$F_{i}\ni\Phi_{i}^{h}\
\ $$h\in F_{j}$

By the definition of a global $(\bm{I};K)$-family of completely separated sets
we get $\Phi_{i}^{h}\in F_{i}$, for every $i\in I$. Moreover,
$\Phi_{j}^{h}=h\circ\lambda_{jj}^{*}=h\circ\mathrm{id}_{\lambda_{0}(j)}=h$. To
show that $\Phi^{h}\in\prod_{i\in I}F_{i}$, let $i,k\in I$ such that
$i=_{(I,K)}k$. By the new condition (b) satisfied by $\boldmath\Lambda^{*}$ we
have that

$\phi^{*}_{ik}\big{(}\Phi^{h}_{i}\big{)}=\phi^{*}_{ik}(h\circ\lambda_{ij}^{*})=h\circ\lambda_{ij}^{*}\circ\lambda_{ki}^{*}=h\circ\lambda_{kj}^{*}=\Phi_{k}^{h}.$

Let $(i,x)=_{{\widehat{K}\cup\widehat{H}}}(j,y)$. By the tightness of
$\neq_{(I,K)}$ we have that

$\forall_{k\in
K}\big{(}\widehat{k}((i,x))=_{{\mathbb{R}}}\widehat{k}((z,y))\big{)}:\Leftrightarrow\forall_{k\in
K}\big{(}k(i)=_{{\mathbb{R}}}k(j)\big{)}\Rightarrow i=_{I}j.$

If $\Phi\in\prod_{i\in I}F_{i}$, then

$\widehat{\Phi}((i,x))=_{{\mathbb{R}}}\widehat{\Phi}((j,y)):\Leftrightarrow\Phi_{i}(x)=_{{\mathbb{R}}}\Phi_{j}(y)\Leftrightarrow\Phi_{j}(y)=_{{\mathbb{R}}}[\phi^{*}_{ij}(\Phi_{j})](x)=\Phi_{j}(\lambda^{*}_{ij}(x)).$

Hence, for every $h\in F_{j}$ we have that
$h(y)=:\Phi_{j}^{h}(y)=_{{\mathbb{R}}}\Phi_{j}^{h}(\lambda^{*}_{ij}(x)):=h\big{(}\lambda^{*}_{ij}(x))\big{)}.$
By the tightness of $\neq_{F_{j}}$ we get the required equality
$y=_{\lambda_{0}(j)}\lambda^{*}_{ij}(x)$. ∎

The importance of the previous theorem lies on the fact that there is no
obvious way to show that the canonical inequality of the Sigma-set of a global
family $\bm{S}^{*}$ of completely separated sets is an apartness relation
using only its definition. The proof of Proposition 2.7 cannot be carried out,
as the transport maps are between any two sets of the given family. By showing
though, that this inequality is equivalent to the inequality induced by
$\widehat{K}\cup\widehat{H}$, then by Remark 3.2(v) this inequality is also an
apartness relation on the Sigma-set of $\bm{S}^{*}$! The reason behind this,
seemingly unexpected, result is the extra information provided by the data
associated to the notion of a global family of completely separated sets.
Through the notion of a global family $\bm{S}^{*}$ of completely separated
sets we can also define when a dependent function over
$\boldmath\Lambda^{*}(\bm{S}^{*})$ is strongly extensional in a way that
generalises the strong extensionality of (non-dependent) functions.

######  Definition 4.9.

If $\boldmath\Lambda^{*}(\bm{S}^{*})$ is a global $\bm{I}$-family of sets with
an inequality, we call a dependent function $\Phi$ in the Pi-set of
$\boldmath\Lambda^{*}(\bm{S}^{*})$ strongly extensional, if

$\forall_{i,j\in
I}\big{(}\lambda_{ij}^{*}(\Phi_{i})\neq_{\lambda_{0}(j)}\Phi_{j}\Rightarrow
i\neq_{(I,K)}j\big{)}.$

Notice that if $\lambda_{ij}^{*}(\Phi_{i})\neq_{\lambda_{0}(j)}\Phi_{j}$, then
$\neg(i=_{I}j)$, as if $i=_{I}j$, then
$\lambda_{ij}^{*}(\Phi_{i})=_{\lambda_{0}(j)}\Phi_{j}$. The above definition
of strong extentionality implies the stronger inequality $i\neq_{I}j$, and
clearly generalises the strong extensionality of non-dependent functions, if a
constant global family of completely separated sets is considered. In analogy
to the strong extensionality of the first projection, we can show that the
second projection $\textnormal{{pr}}_{2}^{\boldmath\Lambda^{*}}$ of the Sigma-
set of $\boldmath\Lambda^{*}(\bm{S}^{*})$, defined as in Definition 2.6, is a
strongly extensional dependent function.

######  Corollary 4.10.

Let $\boldmath\Lambda^{*}$ be a global $\bm{I}$-family of sets with an
inequality.
(i) If $\sigma_{0}\colon\sum_{i\in
I}\lambda_{0}(i)\rightsquigarrow\mathbb{V}_{0}^{\neq}$ is given by
$\sigma_{0}(i,x):=\lambda_{0}(i)$, for every $(i,x)\in\sum_{i\in
I}\lambda_{0}(i)$, and $\sigma^{*}_{(i,x),(j,y)}:=\lambda_{ij}^{*}$, for every
$(i,x),(j,y)\in\sum_{i\in I}\lambda_{0}(i)$, then
$\boldmath\Sigma^{*}:=(\bm{\sigma}_{0},\sigma_{1}^{*})$ is a global
$\bm{I}$-family of sets with an inequality.
(ii) The second projection $\textnormal{{pr}}_{2}^{\boldmath\Lambda^{*}}$ is a
strongly extensional dependent function over $\boldmath\Sigma^{*}$.

###### Proof.

The proof of (i) is immediate. For the proof of (ii), that is

$\textnormal{{pr}}_{2}^{\boldmath\Lambda^{*}}\in\prod_{(i,x)\in\sum_{i\in
I}\lambda_{0}(i)}\sigma_{0}(i,x):=\prod_{(i,x)\in\sum_{i\in
I}\lambda_{0}(i)}\lambda_{0}(i),$

let $(i,x),(j,y)\in\sum_{i\in I}\lambda_{0}(i)$ such that $(i,x)=_{{\sum_{i\in
I}\lambda_{0}(i)}}(j,y)$, that is $i=_{(I,K)}j$ and
$\lambda_{ij}^{*}(x)=_{\lambda_{0}(j)}y$. Then,

$\textnormal{{pr}}_{2}^{\boldmath\Lambda^{*}}(j,y):=y=_{\lambda_{0}(j)}\lambda_{ij}^{*}(x):=\sigma_{(i,x),(j,y)}^{*}\big{(}\textnormal{{pr}}_{2}^{\boldmath\Lambda^{*}}(i,x)\big{)}.$

If $(i,x),(j,y)$ are arbitrary elements of $\sum_{i\in I}\lambda_{0}(i)$, such
that

$\sigma^{*}_{(i,x),(j,y)}\big{(}\textnormal{{pr}}_{2}^{\boldmath\Lambda^{*}}((i,x))\neq_{\sigma_{0}((j,y))}\textnormal{{pr}}_{2}^{\boldmath\Lambda^{*}}((j,y)):\Leftrightarrow\lambda_{ij}^{*}(x)\neq_{\lambda_{0}(j)}y,$

then the inequality $(i,x)\neq_{{\sum_{i\in I}\lambda_{0}(i)}}(j,y)$ follows
immediately. ∎

##  5 The free completely separated set

Next we define the free completely separated set on a given set $(X,=_{X})$.
If $(X,=_{X})$ is in $\mathrm{\mathbf{Set}}$, then by Remark 3.2(iii)
$(X,=_{(X,F)},\neq_{(X,F)};F)$ is in SetComplSep. As $\mathbb{F}(X)$ is an
extensional subset of itself

$\mathbb{F}(X)=\big{\\{}f\in\mathbb{F}(X)\mid f=_{\mathbb{F}(X)}f\big{\\}},$

the structure
$\big{(}X,=_{(X,\mathbb{F}(X))},\neq_{(X,\mathbb{F}(X))};\mathbb{F}(X)\big{)}$
is in SetComplSep.

######  Definition 5.1.

If $(X,=_{X})$ is in $\mathrm{\mathbf{Set}}$, the free completely separated
set on $(X,=_{X})$ is the structure
$\varepsilon\bm{X}:=\big{(}X,=_{(X,\mathbb{F}(X))},\neq_{(X,\mathbb{F}(X))};\mathbb{F}(X)\big{)}$.

######  Theorem 5.2.

(i) $\varepsilon\bm{X}$ has the universal property of the free completely
separated set on $(X,=_{X})$, namely there is a function $i_{X}\colon
X\to|\varepsilon\bm{X}|$ such that for every completely separated set $\bm{Y}$
and function $h\colon X\to|\bm{Y}|$ there is a unique strongly extensional
function $\varepsilon h\colon|\varepsilon\bm{X}|\to|\bm{Y}|$ such the
following triangle commutes

$X$$|\varepsilon\bm{X}|$$|\bm{Y}|$.$i_{X}$$h\ \ $$\varepsilon h$

(ii) Every completely separated set is the quotient of the free completely
separated set over it.
(iii) Let the functor
$\textnormal{{Free}}\colon\mathrm{\mathbf{Set}}\to\textnormal{{SetComplSep}}$,
defined by

$\textnormal{{Free}}(X,=_{X}):=\varepsilon\bm{X},\ \ \
\textnormal{{Free}}(f\colon X\to Y):=\varepsilon
f\colon|\varepsilon\bm{X}|\to|\varepsilon\bm{Y}|$
$X$$|\varepsilon\bm{X}|$$Y$$|\varepsilon\bm{Y}|$,$i_{X}$$f$$i_{Y}$$\varepsilon
f:=\varepsilon(i_{Y}\circ f)$

and let the forgetful functor
$\textnormal{{Frg}}\colon\textnormal{{SetComplSep}}\to\mathrm{\mathbf{Set}}$,
defined by

$\textnormal{{Frg}}\big{(}X,=_{X},\neq_{X};F\big{)}:=(X,=_{X}),\ \ \
\textnormal{{Frg}}(h\colon\bm{X}\to\bm{Y}):=h.$

Then, Free is left adjoint to Frg.

###### Proof.

(i) Let $i_{X}:=\mathrm{id}_{X}$ and $\varepsilon h:=h$. That
$\mathrm{id}_{X}$ is a function follows from Remark 3.2(i). That
$h\colon|\varepsilon\bm{X}|\rightsquigarrow|\bm{Y}|$ is a function, follows
from the fact that every operation from $(X,=_{(X,\mathbb{F}(X))})$ to
$\bm{Y}:=(Y,=_{Y},\neq_{Y};G)$ is a function; if $x,x{{}^{\prime}}\in X$ such
that $x=_{(X,\mathbb{F}(X))}x{{}^{\prime}}$, then
$h(x)=_{Y}h(x{{}^{\prime}})\Leftrightarrow h(x)=_{(Y,G)}h(x{{}^{\prime}})$,
and if $g\in G$, then $g\circ h\in\mathbb{F}(X)$ and the required equality
follows from the hypothesis $x=_{(X,\mathbb{F}(X))}x{{}^{\prime}}$. That
$h\colon|\varepsilon\bm{X}|\rightsquigarrow|\bm{Y}|$ is strongly extensional,
is shown as follows: if $x,x{{}^{\prime}}\in X$, and if $g\in G$ such that
$g\colon h(x)=_{(Y,G)}h(x{{}^{\prime}})$, then $F\ni g\circ h\colon
x\neq_{(X,\mathbb{F}(X))}x{{}^{\prime}}$. The commutativity of the triangle
and the uniqueness of $\varepsilon h$ follow immediately.
(ii) If $\bm{X}:=\big{(}X,=_{X},\neq_{X};F\big{)}$, then the identity
$\mathrm{id}_{X}$ from $\varepsilon\bm{X}$ to $\bm{X}$ is the required
surjection.
(iii) Clearly, Free and Frg are functors. Let
$i_{X,\bm{Y}}\colon\mathrm{Hom}(\varepsilon\bm{X},\bm{Y})\to\mathrm{Hom}(X,\textnormal{{Frg}}(\bm{Y}))$
defined by $i_{X,\bm{Y}}(h):=h$, for every
$h\in\mathrm{Hom}(\varepsilon\bm{X},\bm{Y})$. To show that $i_{X,\bm{Y}}$ is
well-defined, let $x,x{{}^{\prime}}\in X$ with $x=_{X}x{{}^{\prime}}$, hence
$x=_{{(X,\mathbb{F}(X))}}x{{}^{\prime}}$. By our hypothesis on $h$, we get
$h(x)=_{Y}h(x{{}^{\prime}})$. The fact that $i_{X,\bm{Y}}$ is a function, is
trivial to show. Let
$j_{X,\bm{Y}}\colon\mathrm{Hom}(X,\textnormal{{Frg}}(\bm{Y}))\to\mathrm{Hom}(\varepsilon\bm{X},\bm{Y})$
defined by $j_{X,\bm{Y}}(h):=\varepsilon h$, for every
$h\in\mathrm{Hom}(X,\textnormal{{Frg}}(\bm{Y}))$, where $\varepsilon h$ is
determined by the universal property of $\varepsilon\bm{X}$ as follows:

$X$$|\varepsilon\bm{X}|$$Y$$\
|\bm{Y}|$.$i_{X}$$h$$\mathrm{id}_{Y}$$\varepsilon
h:=\varepsilon(\mathrm{id}_{Y}\circ h)$

Clearly, $j_{X,\bm{Y}}$ is a well-defined function, and
$(i_{X,\bm{Y}},j_{X,\bm{Y}})$ witness the equality of the two Hom-sets. If
$\phi\colon X{{}^{\prime}}\to X$, the commutativity of the rectangle

$\mathrm{Hom}(\varepsilon\bm{X},\bm{Y})$$\ \
\mathrm{Hom}(X,\textnormal{{Frg}}(\bm{Y}))$$\mathrm{Hom}(\varepsilon\bm{X}{{}^{\prime}},\bm{Y})$$\mathrm{Hom}(X{{}^{\prime}},\textnormal{{Frg}}(\bm{Y}))$,$i_{X,\bm{Y}}$$\textnormal{{Free}}(\phi)^{*}$$i_{X{{}^{\prime}},\bm{Y}}$$\phi^{*}$

where $\phi^{*}(h):=h\circ\phi=:\textnormal{{Free}}(\phi)^{*}(h)$, follows
easily. Similarly, if $\theta\colon\bm{Y}\to\bm{Y{{}^{\prime}}}$, the
rectangle

$\mathrm{Hom}(\varepsilon\bm{X},\bm{Y})$$\ \
\mathrm{Hom}(X,\textnormal{{Frg}}(\bm{Y}))$$\mathrm{Hom}(\varepsilon\bm{X},\bm{Y}{{}^{\prime}})$$\mathrm{Hom}(X,\textnormal{{Frg}}(\bm{Y}{{}^{\prime}}))$$i_{X,\bm{Y}}$$\theta_{*}$$i_{X,\bm{Y}{{}^{\prime}}}$$\textnormal{{Frg}}(\theta)_{*}$

is commutative, where $\theta_{*}(h):=\theta\circ
h=:\textnormal{{Frg}}(\theta)_{*}(h)$. ∎

Theorem 5.2(i) is the $\mathrm{BST}$-analogue to the (intentional) type-
theoretic fact that the setoid $(X,=_{X})$, where $=_{X}\colon X\to
X\to\mathcal{U}$ is the equality type-family on the type $X\colon\mathcal{U}$,
is the free setoid on $X$ (see [9], p. 74). Its simple proof rests on the
elimination axiom for $=_{X}$, which is a proof-relevant formulation of the
least-reflexive property of $=_{X}$ within intensional $\mathrm{MLTT}$, a
property that cannot be translated directly in $\mathrm{BST}$ (see also [33],
p. 2 and p. 7). As we have noticed after Remark 3.3, the induced equality
$=_{(X,\mathbb{F}(X))}$ is in $\mathrm{BST}$ the “smallest” equality on $X$
induced by real-valued functions on $(X,=_{X})$.

##  6 A set-theoretic Stone-Čech theorem

A completely regular topological space $(X,\mathcal{T})$ is one in which any
pair $(x,B)$, where $B$ is closed and $x\notin B$, is separated by some $f\in
C(X,[0,1])$. The ring of real-valued, continuous functions $C(X)$ of a
completely regular and $T_{1}$-space $X$, also known as a Tychonoff space,
separates the points of $X$, that is

$\forall_{x,x{{}^{\prime}}\in X}\big{(}\forall_{f\in
C(X)}(f(x)=f(x{{}^{\prime}}))\Rightarrow x=x{{}^{\prime}}\big{)}.$

The “sufficiency” of the completely regular topological spaces in the theory
of $C(X)$ is provided by the Stone-Čech theorem, according to which, for every
topological space $X$ there exists a completely regular space $\rho X$ and a
continuous mapping $\tau_{X}\colon X\rightarrow\rho X$ such that the induced
function $f\mapsto\tau^{*}_{X}(f)$, where $\tau^{*}_{X}(f)=f\circ\tau_{X}$, is
a ring isomorphism between $C(\rho X)$ and $C(X)$ (see [GJ60], p.41).

$X$$\rho X$${\mathbb{R}}$$X$$\rho X$$Y$$\tau_{X}$$C(X)\ni\tau^{*}_{X}(f)\ \
$$f\in C(\rho X)$$C(X,Y)\ni h\ \ $$\tau_{X}$$\rho h\in C(\rho X,Y)$

Consequently, a functor $\rho\colon\textnormal{{Top}}\to\textnormal{{crTop}}$
from the category of topological spaces Top to its subcategory of completely
regular topological spaces crTop is defined, which is a reflector, that is for
every continuous function $h$ from $X$ to a completely regular space $Y$ there
is a unique continuous function $\rho h\colon\rho X\to Y$ such that the above
right triangle commutes (see [12], p. 6). Next we present an abstract version
of the Stone-Čech theorem for completely separated sets, which expresses the
corresponding “sufficiency” of completely separated sets. Topological spaces
are replaced by function spaces and completely regular topological spaces by
completely separated sets131313The adverb ”completely“ in the term completely
separated set comes from this analogy.. The category of function spaces was
introduced by Ishihara in [13] without restricting though, to extensional
subsets of $\mathbb{F}(X)$.

######  Definition 6.1.

A function space is a structure $(X,=_{X};F)$, where $(X,=_{X})$ is a set and
$F$ is an extensional subset of $\mathbb{F}(X)$. If $=_{X}$ is clear from the
context, we also write $(X,F)$. In the category FunSpace of function spaces
the arrows are the affine maps, defined in Definition 4.1.

######  Theorem 6.2 (Stone-Čech theorem for function spaces and completely
separated sets).

Let $(X,=_{X};F)$ be a function space.
(i) There is a completely separated set
$\rho_{F}\bm{X}:=\big{(}X,=_{(X,F)},\neq_{(X,F)};\rho F\big{)}$ and a function
$\tau_{X}\colon X\to|\rho_{F}\bm{X}|$ such that $(\tau^{*}_{X},\rho_{X})\colon
F=_{\mathbb{V}_{0}}\rho F$, where $\tau^{*}_{X}\colon\rho F\to F$ is defined
by $\tau^{*}_{X}(g):=g\circ\tau_{X}$, for every $g\in\rho F$, and
$\rho_{X}\colon F\to\rho F$ is defined by $\rho_{X}(f):=f$, for every $f\in
F$. Moreover, every function $f$ in $\rho F$ is strongly extensional.

$X$$|\rho_{F}\bm{X}|$${\mathbb{R}}$$X$$|\rho_{F}\bm{X}|$$|\bm{Y}|$$\tau_{X}$$F\ni\tau^{*}_{X}(f)\
\ $$f\in\rho F$$\mathbb{Af}\big{(}(X;F),(Y;G)\big{)}\ni h\ \ $$\tau_{X}$$\rho
h\in\mathbb{Af}\big{(}(X;\rho F),(Y;G)\big{)}$

(ii) If $\bm{Y}:=(Y,=_{Y},\neq_{Y};G)$ is in SetComplSep and
$h\colon(X,=_{X};F)\to(Y,=_{Y};G)$ is an affine map, there is a unique affine
map $\rho h\colon|\rho_{F}\bm{X}|\to|\bm{Y}|$, such that the above right
triangle commutes.

###### Proof.

(i) Let the assignment routine $\tau_{X}\colon X\rightsquigarrow X$ given by
the identity rule $\tau_{X}(x):=x$, for every $x\in X$. If $X$ is equipped
with the equality $=_{(X,F)}$, let $\rho F$ be the following extensional
subset of $\mathbb{F}(X)$

$\rho F:=\big{\\{}f\colon(X,=_{F})\to({\mathbb{R}},=_{{\mathbb{R}}})\mid
f\circ\tau_{X}\in F\big{\\}}.$

Clearly, the extensionality of $F$ implies the extensionality of $\rho F$, and
$\rho_{F}\bm{X}$ is in SetComplSep as

$\displaystyle x=_{(X,\rho F)}x{{}^{\prime}}$
$\displaystyle:\Leftrightarrow\forall_{f\in\rho
F}\big{(}f(x)=_{{\mathbb{R}}}f(x{{}^{\prime}})\big{)}$
$\displaystyle:\Leftrightarrow\forall_{f\in\rho
F}\big{(}(f\circ\tau_{X})(x)=_{{\mathbb{R}}}(f\circ\tau_{X})(x{{}^{\prime}})\big{)}$
$\displaystyle\Leftrightarrow\forall_{f\in
F}\big{(}f(x)=_{{\mathbb{R}}}f(x{{}^{\prime}})\big{)}$
$\displaystyle\Leftrightarrow:x=_{(X,F)}x{{}^{\prime}}.$

In the non-definitional equivalence above we use the fact that if $f\in\rho
F$, then $f\circ\tau_{X}=f\in F$, and if $f\in F$, then $f\circ\tau_{X}=f\in
F$, and hence $f\in\rho F$. Similarly we show that $x\neq_{(X,\rho
F)}x{{}^{\prime}}\Leftrightarrow x\neq_{(X,F)}x{{}^{\prime}}$. The facts that
$\tau_{X}$ is a function and the pair of functions $(\tau^{*}_{X},\rho_{X})$
witness the equality $F=_{\mathbb{V}_{0}}\rho F$ follow immediately. The
strong extensionality of each $f\in\rho F$ follows immediately from the
equivalence of $\neq_{(X,\rho F)}$ and $\neq_{(X,F)}$.
(ii) Let $\rho h:=h$. To show that $\rho h$ is a function, let
$x=_{(X,F)}x{{}^{\prime}}\Leftrightarrow x=_{(X,\rho F)}x{{}^{\prime}}$. If
$g\in G$, then $g(\rho
h(x)):=g(h(x))=_{{\mathbb{R}}}g(h(x{{}^{\prime}}))=:g(\rho
h(x{{}^{\prime}}))$, as $g\circ h\in F$, hence $g\circ h\in\rho F$.
Consequently, $h(x)=_{Y}h(x{{}^{\prime}})$. The fact that $\rho
h\in\mathbb{Af}\big{(}(X;\rho F),(Y;G)\big{)}$ follows immediately. The
uniqueness of $\rho h$ follows trivially from the definition of $\tau_{X}$ and
the required commutativity of the above right triangle. ∎

From a given set $(X,=_{X})$ and an extensional subset $F$ of $\mathbb{F}(X)$
we constructed a completely separated set $\rho_{F}\bm{X}$ with the same
carrier set $X$ and a larger equality $=_{(X,\rho
F)}\Leftrightarrow=_{(X,F)}$, such that all functions that separate the points
of $(X,=_{(X,\rho F)})$ are strongly extensional. Of course, the inequality
$\neq_{(X,F)}$ is tight with respect to the equality $=_{(X,F)}$. In the proof
of the Stone-Čech theorem for topological spaces and completely regular spaces
$\rho X$ is the the set of equivalence classes of $X$ with respect to the
equivalence relation $x\sim x{{}^{\prime}}:\Leftrightarrow\forall_{f\in
C(X)}\big{(}f(x)=f(x{{}^{\prime}})\big{)}$. Following [14], p. 38, the
quotient of a set over an equivalence relation is treated here as the same
totality with the equivalence relation as its new equality. Clearly, if
$\bm{X}$ is in SetComplSep, the above construction on $(X,=_{F})$ induces
$\bm{X}$ again.

######  Proposition 6.3.

Let the functor
$\rho\colon\textnormal{{FunSpace}}\to\textnormal{{SetAffine}}$, defined by
$\rho(X,=_{X};F):=\rho_{F}\bm{X}$ and
$\rho\big{(}h\colon(X,=_{X};F)\to(Y,=_{Y};G)\big{)}:=\rho
h\colon\rho_{F}\bm{X}\to\rho_{F}\bm{Y}$, where, according to Theorem
6.2$($ii$)$, $\rho h$ is the unique function that makes the following
rectangle commutative

$X$$|\rho_{F}\bm{X}|$$Y$$|\rho_{F}\bm{Y}|$.$\tau_{X}$$h$$\rho h$$\tau_{Y}$

If
$\textnormal{{Emb}}\colon\textnormal{{SetAffine}}\to\textnormal{{FunSpace}}$
is the corresponding embedding functor, defined by
$\textnormal{{Emb}}(\bm{X}):=(X,=_{X};F)$ and
$\textnormal{{Emb}}\big{(}h\colon(\bm{X};F)\to(\bm{Y};G)\big{)}:=h$, then
$\rho$ is left adjoint to Emb, and Emb is left adjoint to $\rho$.

###### Proof.

The fact that $\rho$ is a functor follows immediately by Theorem 6.2$($ii$)$.
From that also follows that SetAffine is reflective in FunSpace, or
equivalently, that $\rho$ is left adjoint to Emb. Next we show that Emb is
left adjoint to $\rho$. We have that

$\mathrm{Hom}\big{(}(\textnormal{{Emb}}(\bm{X}),(Y,=_{Y};G)\big{)}:=\mathbb{Af}\big{(}(X,=_{X};F),(Y,=_{Y};G)\big{)},$
$\mathrm{Hom}\big{(}\bm{X},\rho(Y,=_{Y};G)\big{)}:=\mathbb{Af}\big{(}(X,=_{X},\neq_{X};F),(Y,=_{G},\neq_{G};\rho
G)\big{)}.$

If $h\colon X\to Y$ is in $\mathbb{Af}\big{(}(X,=_{X};F),(Y,=_{Y};G)\big{)}$,
then, for every $g\in\rho G$ we have that $g\circ h=(g\circ\tau_{Y})\circ h\in
F$, as $g\circ\tau_{Y}\in G$ by the definition of $\rho G$. Hence,
$h\in\mathbb{Af}\big{(}(X,=_{X},\neq_{X};F),(Y,=_{G},\neq_{G};\rho G)\big{)}$.
Conversely, if
$h\in\mathbb{Af}\big{(}(X,=_{X},\neq_{X};F),(Y,=_{G},\neq_{G};\rho G)\big{)}$
and $g\in G$, we have that $g\circ h=\rho_{Y}(g)\circ h\in F$, as
$\rho_{Y}(g)\in\rho G$. Hence
$h\in\mathbb{Af}\big{(}(X,=_{X};F),(Y,=_{Y};G)\big{)}$. If
$\phi\colon\bm{X}{{}^{\prime}}\to\bm{X}$ and
$\theta\colon(Y,=_{Y};G)\to(Y{{}^{\prime}},=_{Y{{}^{\prime}}};G{{}^{\prime}})$
are affine

$\mathrm{Hom}(\textnormal{{Emb}}(\bm{X}),(Y,=_{Y};G))$$\
\mathrm{Hom}(\bm{X},\rho_{G}\bm{Y})$$\
\mathrm{Hom}(\textnormal{{Emb}}(\bm{X}{{}^{\prime}}),(Y,=_{Y};G)$$\mathrm{Hom}(\bm{X}{{}^{\prime}},\rho_{G}\bm{Y})$$\mathrm{id}$$\textnormal{{Emb}}(\phi)^{*}$$\mathrm{id}$$\phi^{*}$$\mathrm{Hom}(\textnormal{{Emb}}(\bm{X}),(Y,=_{Y};G))\
\ $$\ \ \ \mathrm{Hom}(\bm{X},\rho_{G}\bm{Y})$$\ \
\mathrm{Hom}(\textnormal{{Emb}}(\bm{X}),(Y{{}^{\prime}},=_{Y{{}^{\prime}}};G{{}^{\prime}}))$$\mathrm{Hom}(\bm{X},\rho_{G{{}^{\prime}}}\bm{Y}{{}^{\prime}})$$\mathrm{id}$$\theta_{*}$$\mathrm{id}$$(\rho\theta)_{*}$

the commutativity of the above rectangles is straightforward to show. ∎

It is not often the case that we have functors like $\rho$ and Emb, such that
$\rho\dashv\textnormal{{Emb}}\dashv\rho$. For example, although in Theorem
5.2(iii) we showed that $\textnormal{{Free}}\dashv\textnormal{{Frg}}$, we
cannot show that $\textnormal{{Frg}}\dashv\textnormal{{Free}}$. Because of the
relations $\rho\dashv\textnormal{{Emb}}\dashv\rho$, we have that $\rho$
preserves all limits and colimits. For example, as $(X\times Y,=_{X\times
Y};F\otimes G)$ is the product of $(X,=_{X};F)$ and $(Y,=_{Y},;G)$ in
FunSpace, we have that $\rho_{F\otimes
G}(\bm{X}\times\bm{Y})=\rho_{F}(\bm{X})\times\rho_{G}(\bm{Y})$.

##  7 A set-theoretic Tychonoff embedding theorem

According to the classical Tychonoff embedding theorem, a $T_{1}$ topological
space is completely regular if and only if it is topologically embedded into a
product of $[0,1]$ equipped with its standard topology. Here we give a purely
set-theoretic formulation of this result within $\mathrm{BST}$. As the
separating functions considered here take values in ${\mathbb{R}}$, the
corresponding product will be a (dependent) product of ${\mathbb{R}}$. As in
the previous section, we replace complete regularity by complete separation.

######  Lemma 7.1.

Let $\bm{X},\bm{I}$ be in SetIneq and
$\boldmath\Lambda:=(\lambda_{0},\lambda_{1})$ a family of sets with an
inequality over $\bm{I}$. If $\boldmath M:=(\bm{\mu}_{0},\mu_{1})$, where
$\bm{\mu}_{0}\colon I\rightsquigarrow\mathbb{V}_{0}^{\neq}$ is defined by
$\overline{\mu}_{0}(i):=\big{(}\mathbb{F}(X,\lambda_{0}(i)),=_{\mathbb{F}(X,\lambda_{0}(i))},\neq_{\mathbb{F}(X,\lambda_{0}(i))}\big{)}$
and

$\mu_{1}\colon\bigcurlywedge_{(i,j)\in
D(I)}\mathbb{F}^{\neq}\big{(}\mathbb{F}(X,\lambda_{0}(i)),\mathbb{F}(X,\lambda_{0}(j))\big{)},\
\ \ \mu_{1}(i,j):=\mu_{ij},\ \ \ (i,j)\in D(I),$
$\mu_{ij}\colon\mathbb{F}(X,\lambda_{0}(i))\to\mathbb{F}(X,\lambda_{0}(j)),\ \
\ \ \mu_{ij}(\phi):=\lambda_{ij}\circ\phi,\ \ \
\phi\in\mathbb{F}(X,\lambda_{0}(i))$
$X$$\lambda_{0}(i)$$\lambda_{0}(j)$,$\phi$$\mu_{ij}(\phi)\ \ $$\lambda_{ij}$

then $\boldmath M$ is a family of sets with an inequality over $\bm{I}$.

###### Proof.

If $i\in I$, then
$\mu_{ii}(\phi):=\lambda_{ii}\circ\phi=\mathrm{id}_{\lambda_{0}(i)}\circ\phi=\phi$,
for every $\phi\in\mathbb{F}(X,\lambda_{0}(i))$. If $i=_{I}j=_{I}k$, then

$\mathbb{F}(X,\lambda_{0}(j))$$\mathbb{F}(X,\lambda_{0}(k)).$$\mathbb{F}(X,\lambda_{0}(i))$$\mu_{jk}$$\mu_{ij}$$\
\ \mu_{ik}$

$(\mu_{jk}\circ\mu_{ij})(\phi):=\mu_{jk}\big{(}\lambda_{ij}\circ\phi):=\lambda_{jk}\circ\big{(}\lambda_{ij}\circ\phi)=\lambda_{ij}\circ\phi=:\mu_{ik}(\phi),$
for every $\phi\in\mathbb{F}(X,\lambda_{0}(i))$. To show that $\mu_{ij}$ is
strongly extensional, let
$\phi,\phi{{}^{\prime}}\in\mathbb{F}(X,\lambda_{0}(i))$. As $\lambda_{ij}$ is
strongly extensional, we have that

$\displaystyle\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\mu_{ij}(\phi)\neq_{\mathbb{F}(X,\lambda_{0}(i))}\mu_{ij}(\phi{{}^{\prime}})$
$\displaystyle:\Leftrightarrow\lambda_{ij}\circ\phi\neq_{\mathbb{F}(X,\lambda_{0}(i))}\lambda_{ij}\circ\phi{{}^{\prime}}$
$\displaystyle:\Leftrightarrow\exists_{x\in
X}\big{(}\lambda_{ij}(\phi(x))\neq_{\lambda_{0}(j)}\lambda_{ij}(\phi(x{{}^{\prime}}))\big{)}$
$\displaystyle\Rightarrow\exists_{x\in
X}\big{(}\phi(x)\neq_{\lambda_{0}(i)}\phi(x{{}^{\prime}})\big{)}$
$\displaystyle:\Leftrightarrow\phi\neq_{\mathbb{F}(X,\lambda_{0}(i))}\phi{{}^{\prime}}.\
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\qed$

######  Theorem 7.2 (Embedding lemma for sets with an inequality).

Let $\bm{X},\bm{I}$ be in SetIneq and
$\boldmath\Lambda:=(\lambda_{0},\lambda_{1})$ a family of sets with an
inequality over $\bm{I}$. Let also $H\in\prod_{i\in I}\mu_{0}(i)$, where
$\boldmath M:=(\mu_{0},\mu_{1})$ is the family of sets with inequality over
$\bm{I}$ defined in Lemma 7.1. If

$\prod_{I}\Lambda:=\bigg{(}\prod_{i\in I}\lambda_{0}(i),=_{\prod_{i\in
I}\lambda_{0}(i)},\neq_{\prod_{i\in I}\lambda_{0}(i)}\bigg{)},$

let the assignment routine

$e^{H}\colon X\rightsquigarrow\prod_{i\in I}\lambda_{0}(i),\ \ \ x\mapsto
e^{H}(x),$ $\big{[}e^{H}(x)\big{]}_{i}:=H_{i}(x),\ \ \ i\in I.$

(i) $e^{H}$ is a well-defined function.
(ii) Let the extensional subset $\Phi:=\\{e^{H}\\}$ of
$\mathbb{F}\big{(}X,\prod_{i\in I}\lambda_{0}(i)\big{)}$. If the induced
inequality $\neq_{(X,\Phi)}$ on $X$ is tight, then $e^{H}$ is an embedding,
and if $H_{i}$ is strongly extensional, for every $i\in I$, then $e^{H}$ is
strongly extensional.

###### Proof.

(i) First we show that $e^{H}$ is well-defined, that is $e^{H}\in\prod_{i\in
I}\lambda_{0}(i)$. If $i=_{I}j$, then

$\big{[}e^{H}(x)\big{]}_{j}:=H_{j}(x)=_{\lambda_{0}(j)}\big{[}(\mu_{ij}(H_{i})\big{]}(x):=[\lambda_{ij}\circ
H_{i}](x):=\lambda_{ij}\big{(}H_{i}(x)\big{)}=:\lambda_{ij}\big{(}\big{[}e^{H}(x)\big{]}_{i}\big{]}.$

If $x=_{X}x{{}^{\prime}}$, then $e^{H}(x)=_{\prod_{i\in
I}\lambda_{0}(i)}e^{H}(x{{}^{\prime}})$, as for every $i\in I$ we have that
$H_{i}(x)=_{\lambda_{0}(i)}H_{i}(x{{}^{\prime}})$.
(ii) The tightness of $\neq_{(X,\Phi)}$ means that
$x=_{(X,\Phi)}x{{}^{\prime}}\Rightarrow x=_{X}x{{}^{\prime}}$, for every
$x,x{{}^{\prime}}\in X$, where

$\displaystyle x=_{(X,\Phi)}x{{}^{\prime}}$ $\displaystyle:\Leftrightarrow
e^{H}(x)=_{\prod_{i\in I}\lambda_{0}(i)}e^{H}(x{{}^{\prime}})$
$\displaystyle:\Leftrightarrow\forall_{i\in
I}\big{(}\big{[}e^{H}(x)\big{]}_{i}=_{\lambda_{0}(i)}\big{[}e^{H}(x{{}^{\prime}})\big{]}_{i}$
$\displaystyle:\Leftrightarrow\forall_{i\in
I}\big{(}H_{i}(x)=_{\lambda_{0}(i)}H_{i}(x{{}^{\prime}})\big{)}.$

Hence, $e^{H}(x)=_{\prod_{i\in
I}\lambda_{0}(i)}e^{H}(x{{}^{\prime}})\Rightarrow x=_{X}x{{}^{\prime}}$
follows immediately. If each $H_{i}$ is strongly extensional, then

$\displaystyle\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
e^{H}(x)\neq_{\prod_{i\in I}\lambda_{0}(i)}e^{H}(x{{}^{\prime}})$
$\displaystyle:\Leftrightarrow\exists_{i\in
I}\big{(}\big{[}e^{H}(x)\big{]}_{i}\neq_{\lambda_{0}(i)}\big{[}e^{H}(x{{}^{\prime}})\big{]}_{i}$
$\displaystyle:\Leftrightarrow\exists_{i\in
I}\big{(}H_{i}(x)\neq_{\lambda_{0}(i)}H_{i}(x{{}^{\prime}})\big{)}$
$\displaystyle\Rightarrow x\neq_{X}x{{}^{\prime}}.\ \ \ \ \ \ \ \ \ \ \ \ \ \
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\ \ \ \ \ \ \ \qed$

######  Definition 7.3.

If $(X,=_{X};F)$ is a function space, its dual completely separated set is the
structure $\bm{X}^{*}:=(F,=_{F},\neq_{F};\widehat{X})$, where $=_{F}$ and
$\neq_{F}$ are induced by $\mathbb{F}(X)$, and

$\widehat{X}:=\\{\widehat{x}\mid x\in X\\},\ \ \ \ \widehat{x}\colon
F\to{\mathbb{R}},\ \ \ \widehat{x}(f):=f(x);\ \ \ f\in F,\ x\in X.$

The contravariant functor
$\textnormal{{Dual}}\colon\textnormal{{FunSpace}}^{\mathrm{op}}\to\textnormal{{SetAffine}}$
is defined by $\textnormal{{Dual}}(X,=_{X};F):=\bm{X}^{*}$ and
$\textnormal{{Dual}}\big{(}h\colon(X,=_{X};F)\to(Y,=_{Y};G)\big{)}:=h^{*}\colon\bm{Y}^{*}\to\bm{X}^{*}$,
where $h^{*}(g):=g\circ h\in F$, for every $g\in G$.

Clearly, one can “identify” $(X,=_{X};F)$ with
$(\widehat{X},=_{\widehat{X}};\widehat{F})$, where
$\widehat{F}:=\\{\widehat{f}\mid f\in F\\}$ and
$\widehat{f}(\widehat{x}):=\widehat{x}(\widehat{f}):=f(x)$, for every $f\in F$
and $x\in X$, as the maps $x\mapsto\widehat{x}$ and $\widehat{x}\mapsto x$
form an iso in the category FunSpace.

######  Remark 7.4.

Let $(X,=_{X};F)$ be a function space.
(i) Let $\bm{\lambda}_{0}(f):=\bm{R}$, for every $f\in F$, and
$\lambda_{fg}:=\mathrm{id}_{{\mathbb{R}}}$, for every $f,g\in F$ such that
$f=_{F}g$. Moreover, let $\phi_{0}(f):=\\{\mathrm{id}_{{\mathbb{R}}}\\}$, for
every $f\in F$ and, if $f=_{F}g$, let
$\phi_{fg}\colon\\{\mathrm{id}_{{\mathbb{R}}}\\}\to\\{\mathrm{id}_{{\mathbb{R}}}\\}$
be given by the identity rule. Then the structure
$\bm{S}:=(\lambda_{0},\lambda_{1};\phi_{0},\phi_{1})$ is a family of
complemented sets over the dual completely separated set
$\bm{X}^{*}:=(\bm{F};\widehat{X})$ of the function space $(X,=_{X};F)$.
(ii) If
$\bm{R}^{F}:=\big{(}{\mathbb{R}}^{F},=_{{\mathbb{R}}^{F}},\neq_{{\mathbb{R}}^{F}};\bigotimes_{f\in
F}\\{\mathrm{id}_{{\mathbb{R}}}\\}\big{)},$ where

$\bigotimes_{f\in
F}\\{\mathrm{id}_{{\mathbb{R}}}\\}:=\big{\\{}\mathrm{id}_{{\mathbb{R}}}\circ\textnormal{{pr}}_{f}^{\boldmath\Lambda}=\textnormal{{pr}}_{f}^{\boldmath\Lambda}\mid
f\in F\big{\\}},$

then $\bm{R}^{F}\in\textnormal{{SetComplSep}}$.

###### Proof.

The proof of case (i) is straightforward and case (ii) follows from case (i)
and Proposition 4.5. ∎

Clearly, if $(X,=_{X})$ is in $\mathrm{\mathbf{Set}}$, and $\neq_{(X,F)}$ is
tight, then $(X,=_{X},\neq_{(X,F)};F)$ is in SetComplSep.

######  Theorem 7.5 (Tychonoff embedding theorem for function spaces and
completely separated sets).

Let $(X,=_{X};F)$ be a function space.
(i) If the induced inequality $\neq_{(X,F)}$ on $X$ is tight, then there is an
affine embedding $($injection$)$ of the completely separated set
$(X,=_{X},\neq_{(X,F)};F)$ into the completely separated set $\bm{R}^{F}$.
(ii) If
$e\colon(X,=_{X};F)\to({\mathbb{R}}^{F},=_{{\mathbb{R}}^{F}};\bigotimes_{f\in
F}\\{\mathrm{id}_{{\mathbb{R}}}\\})$ is an affine embedding, then the induced
inequality $\neq_{(X,F)}$ on $X$ is tight, and hence
$(X,=_{X},\neq_{(X,F)};F)$ is in SetComplSep.

###### Proof.

(i) Let $\boldmath M:=(\mu_{0},\mu_{1})$ be the family of sets over $\bm{F}$
from Lemma 7.1 that corresponds to the constant $\bm{F}$-family of sets with
an inequality $(\lambda_{0},\lambda_{1})$ in Remark 7.4(i). Let the dependent
function

$H(F)\colon\prod_{f\in F}\mu_{0}(f):=\prod_{f\in
F}\mathbb{F}(X,{\mathbb{R}}),$ $H(F)_{f}:=f,\ \ \ \ f\in F.$

If $f=_{F}g$, then
$H^{F}_{g}:=g=_{F}f=:H(F)_{f}:=\mathrm{id}_{{\mathbb{R}}}\circ
H(F)_{f}:=\lambda_{fg}\circ H(F)_{f}:=\mu_{fg}\big{(}H(F)_{f}\big{)}$, hence
$H(F)$ is well defined. By Theorem 7.2(i) we get the function

$e^{H(F)}\colon X\to\prod_{f\in F}{\mathbb{R}}=:{\mathbb{R}}^{F},\ \ \
x\mapsto e^{H(F)}(x),$ $\big{[}e^{H(F)}(x)\big{]}_{f}:=H(F)_{f}(x):=f(x),\ \ \
f\in F,\ x\in X.$

Next we show that the inequality $\neq_{(X,\Phi)}$ on $X$, where
$\Phi:=\\{e^{H(F)}\\}$, is tight. If $x,x{{}^{\prime}}\in X$, then

$\displaystyle x=_{(X,\Phi)}x{{}^{\prime}}$ $\displaystyle:\Leftrightarrow
e^{H(F)}(x)=_{{\mathbb{R}}^{F}}e^{H(F)}(x{{}^{\prime}})$
$\displaystyle:\Leftrightarrow\forall_{f\in
F}\big{(}\big{[}e^{H(F)}(x)\big{]}_{f}=_{{\mathbb{R}}}\big{[}e^{H(F)}(x{{}^{\prime}})\big{]}_{f}\big{)}$
$\displaystyle:\Leftrightarrow\forall_{f\in
F}\big{(}f(x)=_{{\mathbb{R}}}f(x{{}^{\prime}})\big{)}$
$\displaystyle:\Leftrightarrow x=_{F}x{{}^{\prime}}$ $\displaystyle\Rightarrow
x=_{X}x{{}^{\prime}},$

where the last implication follows from the tightness of $\neq_{(X,F)}$. To
show that $e^{H(F)}$ is affine, it suffices to show that
$\textnormal{{pr}}_{f}^{\boldmath\Lambda}\circ e^{H(F)}\in F$, for every $f\in
F$. By the definition of $e^{H(F)}$ though, we have that
$\textnormal{{pr}}_{f}^{\boldmath\Lambda}\circ e^{H(F)}=_{F}f\in F$.
(ii) If $x,x{{}^{\prime}}\in X$ such that $x=_{(X,F)}x{{}^{\prime}}$. we show
that $x=_{X}x{{}^{\prime}}$. As $e$ is an embedding, it suffices to show that
$e(x)=_{{\mathbb{R}}^{F}}e(x{{}^{\prime}})\Leftrightarrow
e(x)=_{\bigotimes_{f\in
F}\\{\mathrm{id}_{{\mathbb{R}}}\\}}e(x{{}^{\prime}})\Leftrightarrow\forall_{f\in
F}\big{(}\textnormal{{pr}}_{f}^{\boldmath\Lambda}(e(x))=_{{\mathbb{R}}}\textnormal{{pr}}_{f}^{\boldmath\Lambda}(e(x{{}^{\prime}}))\big{)}$.
As $e$ is affine, the composition
$\textnormal{{pr}}_{f}^{\boldmath\Lambda}\circ e$ is in $F$, for every $f\in
F$, and we use the hypothesis $x=_{(X,F)}x{{}^{\prime}}$. ∎

Notice that in the above proof we avoided negation completely. Theorem 7.5
offers a criterion for the generation of a completely separated set
$(X,=_{X},\neq_{(X,F)};F)$ from a given function space $(X,=_{X};F)$.

##  8 Concluding remarks

In this paper we begun the study of completely separated sets within
$\mathrm{BST}$, realising both the attitude within $\mathrm{CM}$ of using
positive definitions, instead of negative ones, and the attitude of employing
functions, instead of sets, whenever that is possible. Completely separated
sets are equipped with a positive notion of an inequality, as their given
inequality is equivalent to the inequality induced by a set of real-valued
functions. Showing that a set with an inequality $(X,=_{X},\neq_{X})$ is
completely separated, by finding an extensional subset $F$ of $\mathbb{F}(X)$
such that $=_{X}$ is equivalent to $=_{(X,F)}$ and $\neq_{X}$ is equivalent to
$\neq_{(X,F)}$, is a method of proving that $\neq_{X}$ is an apartness, and
hence an extentional relation. As we saw in the case of Theorem 4.8, to prove
directly that $\neq_{X}$ is an apartness relation can be non-trivial.

The various distinctions that are made possible within $\mathrm{CM}$
facilitate the definition of interesting, new categories of sets, such as the
category SetIneq of sets with an inequality, and the categories SetComplSep
and SetAffine of completely separated and affine sets, respectively. If
$(\bm{C}\subseteq\bm{D})\ \bm{C}\subset\bm{D}$ denotes that $\bm{C}$ is a
(full) subcategory of $\bm{D}$, we have that

$\textnormal{{SetAffine}}\subset\textnormal{{SetComplSep}}\subseteq\textnormal{{SetIneq}}.$

We defined the corresponding notions of families of sets in these categories
and their Pi- and Sigma-sets, extending141414We also added two more open-ended
universes in $\mathrm{BST}$, the universe $\mathbb{V}_{0}^{\neq}$ of
predicative sets with an inequality and the universe of completely separated
sets $\mathbb{V}_{0}^{\textnormal{{f}}}$. Clearly, both of them are proper
classes. in this way our previous work [33]. We also introduced the notions of
a global family of sets with an inequality over an index-set with an
inequality and of a global family of completely separated sets over an index-
completely separated set, in order to describe the Sigma-set of the latter.
Global families helped us to formulate a notion of strong extensionality for
dependent functions that generalises the strong extensionality of non-
dependent functions. The free completely separated set on a given set gave us
a way to translate into $\mathrm{BST}$ the freeness of the equality setoid on
a given type within intentional $\mathrm{MLTT}$. We also provided purely set-
theoretic versions of the classical Stone-Čech theorem and the Tychonoff
embedding theorem for completely regular spaces, by replacing topological
spaces with function spaces and completely regular spaces with completely
separated sets

$\frac{\textnormal{{SetComplSep}}}{\textnormal{{FunSpace}}}\approx\frac{\textnormal{{crTop}}}{\textnormal{{Top}}}.$

Although we cannot show constructively that all real-valued functions on a
function space $(X,=_{X};F)$ are strongly extensional, by Theorem 6.2 we can
always find a new equality on $X$ such that all elements of $F$ become
strongly extensional! The positive formulation of our basic concepts also
helped us to avoid negation in the proofs of Theorems 6.2 and 7.5. If the set
$F$ in a function space is closed under the minimum operation, namely
$P_{F}(f)\ \&\ P_{F}(g)\Rightarrow P_{F}(f\wedge g)$, where $f\wedge
g:=\min\\{f,g\\}$, and if for every $x\in X$ there is some $f\in F$ such that
$f(x)>0$, then the family $(U(f))_{f\in F}$, where

$U(f)=\\{x\in X\mid f(x)>0\\},$

is a base for a topology of open sets on $X$. The tightness of the inequality
$\neq_{(X,F)}$ is equivalent then to the topological fact that each singleton
$\\{x\\}$ in $X$ is a closed set (see Proposition 3.5 in [36]). Theorems 6.2
and 7.5 can also be seen as purely set-theoretic versions of the constructive
Stone-Čech theorem and the Tychonoff embedding theorem for Bishop spaces in
[24, 25].

The categories
$\mathrm{\mathbf{Set}},\textnormal{{SetIneq}},\textnormal{{SetComplSep}}$ and
SetAffine need to be studied further, and to be connected with the elaboration
of abstract category theory within $\mathrm{BST}$ in [40]. The theory of
(global) families of completely separated sets is expected to be developed in
line of the general theory of families of sets in [33]. The arrows between
these families, the corresponding distributivity of the Pi-set over the Sigma-
set, and the families of subsets of a completely separated set, are some of
the topics to be studied along the lines of [33]. Inequalities are easier to
study in $\mathrm{BST}$, rather than in (intensional) $\mathrm{MLTT}$. Also,
the notion of a global family of completely separated sets over an index-
completely separated set seems to have no (intentional) type-theoretic
analogue. The question whether the above categories of sets with an
inequality, and the notions of their indexed families studied here, can be
grasped by intensional $\mathrm{MLTT}$, seems to us both interesting and hard.

## References

  * [1] P. Aczel, M. Rathjen: Constructive Set Theory, book draft, 2010.
  * [2] S. Awodey: Category Theory, Oxford University Press, 2010.
  * [3] E. Bishop: Foundations of Constructive Analysis, McGraw-Hill, 1967.
  * [4] E. Bishop, H. Cheng: Constructive Measure Theory, Mem. Amer. Math. Soc. 116, 1972.
  * [5] E. Bishop, D. S. Bridges: Constructive Analysis, Grundlehren der Math. Wissenschaften 279, Springer-Verlag, Heidelberg-Berlin-New York, 1985.
  * [6] D. S. Bridges: Reflections on function spaces, Annals of Pure and Applied Logic 163, 2012, 101-110.
  * [7] D. S. Bridges, F. Richman: Varieties of Constructive Mathematics, Cambridge University Press, 1987.
  * [8] T. Coquand: Universe of Bishop sets, manuscript, 2017.
  * [9] T. Coquand, P. Dybjer, E. Palmgren, A. Setzer: Type-theoretic Foundations of Constructive Mathematics, book-draft, 2005.
  * [10] H. Diener: Constructive Reverse Mathematics, arXiv:1804.05495, 2020.
  * [11] S. Feferman: Constructive theories of functions and classes, in Boffa et al. (Eds.) Logic Colloquium 78, North-Holland, 1979, 159–224.
  * [12] H. Herrlich: Topologische Reflexionen und Coreflexionen, Lecture Notes in Mathematics, Springer, 1968.
  * [13] H. Ishihara: Relating Bishop’s function spaces to neighborhood spaces, Annals of Pure and Applied Logic 164, 2013, 482-490.
  * [14] R. Mines, F. Richman, W. Ruitenburg: A Course in Constructive Algebra, Springer, 1988.
  * [15] P. Martin-Löf: An intuitionistic theory of types: predicative part, in H. E. Rose and J. C. Shepherdson (Eds.) Logic Colloquium’73, Proceedings of the Logic Colloquium, volume 80 of Studies in Logic and the Foundations of Mathematics, pp.73-118, North-Holland, 1975.
  * [16] P. Martin-Löf: An intuitionistic theory of types, in G. Sambin, J. M. Smith (Eds.) Twenty-five years of constructive type theory (Venice, 1995), volume 36 of Oxford Logic Guides, Oxford University Press, 1998, 127–172.
  * [17] J. Myhill: Constructive Set Theory, J. Symbolic Logic 40, 1975, 347–382.
  * [18] E. Palmgren: Bishop’s set theory, Slides from TYPES Summer School 2005, Gothenburg, in http://staff.math.su.se/palmgren/, 2005.
  * [19] E. Palmgren: Proof-relevance of families of setoids and identity in type theory, Arch. Math. Logic, 51, 2012, 35-47.
  * [20] E. Palmgren: Constructivist and structuralist foundations: Bishop’s and Lawvere’s theories of sets, Annals of Pure and Applied Logic 163, 2012, 1384–1399.
  * [21] E. Palmgren: Bishop-style constructive mathematics in type theory - A tutorial, Slides, in http://staff.math.su.se/palmgren/, 2013.
  * [22] E. Palmgren: Lecture Notes on Type Theory, 2014.
  * [23] E. Palmgren, O. Wilander: Constructing categories and setoids of setoids in type theory, Logical Methods in Computer Science. 10 (2014), Issue 3, paper 25.
  * [24] I. Petrakis: Constructive Topology of Bishop Spaces, PhD Thesis, LMU Munich, 2015.
  * [25] I. Petrakis: Completely Regular Bishop Spaces, in A. Beckmann, V. Mitrana and M. Soskova (Eds.): Evolving Computability, CiE 2015, LNCS 9136, 2015, 302–312.
  * [26] I. Petrakis: The Urysohn Extension Theorem for Bishop Spaces, in S. Artemov, A. Nerode (Eds.) Symposium on Logical Foundations in Computer Science 2016, LNCS 9537, 2016, 299–316.
  * [27] I. Petrakis: A constructive function-theoretic approach to topological compactness, Proceedings of the 31st Annual ACM-IEEEE Symposium on Logic in Computer Science (LICS 2016), July 5-8, 2016, NYC, USA, 605–614.
  * [28] I. Petrakis: Constructive uniformities of pseudometrics and Bishop topologies, Journal of Logic and Analysis, 11:FT2, 2019, 1–44.
  * [29] I. Petrakis: Dependent sums and Dependent Products in Bishop’s Set Theory, in P. Dybjer et. al. (Eds) TYPES 2018, LIPIcs, Vol. 130, Article No. 3, 2019.
  * [30] I. Petrakis: Borel and Baire sets in Bishop Spaces, in F. Manea et. al. (Eds): Computing with Foresight and Industry, CiE 2019, LNCS 11558, Springer, 2019, 240–252.
  * [31] I. Petrakis: Embeddings of Bishop spaces, Journal of Logic and Computation, exaa015, 2020, https://doi.org/10.1093/logcom/exaa015.
  * [32] I. Petrakis: Functions of Baire-class one over a Bishop topology, in M. Anselmo et. al. (Eds.) Beyond the Horizon of Computability CiE 2020, LNCS 12098, 215–227.
  * [33] I. Petrakis: Families of Sets in Bishop Set Theory, Habilitationsschrift, LMU, Munich, 2020, available at https://www.mathematik.uni-muenchen.de/$\sim$petrakis/.
  * [34] I. Petrakis: Direct spectra of Bishop spaces and their limits, Logical Methods in Computer Science, Volume 17, Issue 2, 2021, pp. 4:1-4:50.
  * [35] I. Petrakis: Proof-relevance in Bishop-style constructive mathematics, Mathematical Structures in Computer Science, 2022, to appear, doi:10.1017/S0960129522000159.
  * [36] I. Petrakis: Closed subsets in Bishop topological groups, submitted, 2022.
  * [37] I. Petrakis: Strong negation in constructive mathematics, in preparation, 2022.
  * [38] I. Petrakis: On the definition of Bishop sets, in preparation, 2022.
  * [39] I. Petrakis: From Daniell spaces to the integration spaces of Bishop and Cheng, in preparation, 2022.
  * [40] I. Petrakis: Category Theory in Bishop Set Theory, in preparation, 2022.
  * [41] I. Petrakis: Bases of pseudocompact Bishop spaces, in D. S. Bridges et.al (Eds.) Handbook of Constructive Mathematics, Cambridge University Press, 2023, to appear.
  * [42] I. Petrakis, D. Wessel: Algebras of complemented subsets, in U. Berger et.al. (Eds): Revolutions and Revelations in Computability, CiE 2022, LNCS 13359, Springer, 2022, 246–258.
  * [43] I. Petrakis, M. Zeuner: Pre-measure spaces and pre-integration spaces in predicative Bishop-Cheng measure theory, arXiv:2207.08684, 2022.
  * [44] F. Richman: Constructive mathematics without choice, in [46], pp. 199–205.
  * [45] W. Ruitenburg: Inequality in Constructive Mathematics, Notre Dame Journal of Formal Logic, Vol. 32 (4), 1991, 533–553.
  * [46] P. Schuster, U. Berger and H. Osswald (Eds.): Reuniting the Antipodes Constructive and Nonstandard Views of the Continuum, Dordrecht: Kluwer, 2001.
  * [47] M. Shulman: Affine Logic for Constructive Mathematics, arXiv:1805.07518v2, 2021.