# Closed subsets in Bishop topological groups

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

We introduce the notion of a Bishop topological group i.e., a group $X$
equipped with a Bishop topology of functions $F$ such that the group
operations of $X$ are Bishop morphisms with respect to $F$. A closed subset in
the neighborhood structure of $X$ induced by its Bishop topology $F$ is
defined in a positive way i.e., not as the complement of an open subset in
$X$. The corresponding closure operator, although it is not topological, in
the classical sense, does not involve sequences. As countable choice (CC) is
avoided, and in agreement with Richman’s critique on the use of CC in
constructive mathematics, the fundamental facts on closed subsets in Bishop
topological groups shown here have a clear algorithmic content. We work within
Bishop’s informal system of constructive mathematics $\mathrm{BISH}$, without
countable choice, equipped with inductive definitions with rules of countably
many premises.

##  1 Introduction

The constructive non-viability of the notion of topological space is
corroborated by the fact that many classical topological phenomena, like the
duality between open and closed sets, are compatible only with classical
logic. In a straightforward, constructive translation of general topology we
cannot accept that the set-theoretic complement of a closed set is open. E.g.,
$\\{0\\}$ is a closed subset ${\mathbb{R}}$, with respect to the topology on
${\mathbb{R}}$ induced by its standard metric, while its complement cannot be
accepted constructively as open, since that would imply the implication
$\neg(x=0)\Rightarrow(x>0\vee x<0),$ which is (constructively) equivalent to
the constructively unacceptable principle of Markov (see [6], p. 15). The
standard use of negative definitions in classical topology does not permit a
smooth translation of classical topology to a constructive framework.

In [3], chapter 3, Bishop defined a neighbourhood space
$\mathcal{N}:=(X,I,\nu)$, where $X,I$ are sets, and $(\nu_{i})_{i\in I}$ is a
family of subsets of $X$ indexed by $I$ (see [36] for an elaborate study of
this notion) that satisfies the following covering $(\mathrm{NS}_{1})$ and
neighborhood-condition $(\mathrm{NS}_{2})$:
$(\mathrm{NS}_{1})$ $\bigcup_{i\in I}\nu(i)=X$.
$(\mathrm{NS}_{2})$ $\forall_{x\in X}\forall_{i,j\in
I}\big{[}x\in\nu(i)\cap\nu(j)\Rightarrow\exists_{k\in I}\big{(}x\in\nu(k)\ \&\
\nu(k)\subseteq\nu(i)\cap\nu(j)\big{)}\big{]}$.
A subset $O$ of $X$ is called $\nu$-open, if $\forall_{x\in O}\exists_{i\in
I}\big{(}x\in\nu(i)\ \&\ \nu(i)\subseteq O\big{)}$. An $\nu$-closed set $C$ is
not defined negatively, as the complement of a $\nu$-open set, but positively
by the condition

$\forall_{x\in X}\big{(}x\in\overline{C}\Rightarrow x\in C\big{)},$
$x\in\overline{C}:\Leftrightarrow\forall_{i\in
I}(x\in\nu(i)\Rightarrow\nu(i)\between C),$

where, if $A,B$ are subsets of $X$, then $A\between
B:\Leftrightarrow\exists_{y\in X}(y\in A\cap B)$. If $(Y,J,\mu)$ is a
neighborhood space, a function $h:X\to Y$ is neighborhood-continuous, if
$h^{-1}(\mu(j))$ is $\nu$-open, for every $j\in J$. The concept of
neighborhood space was proposed as a set-theoretic alternative to the notion
of topological space, and it is a formal topology in the sense of Sambin [38],
[39].

In [3], chapter 3, Bishop also defined the notion of function space
$\mathcal{F}:=(X,F)$, where $X$ is a set and $F$ is a subset of
$\mathbb{F}(X)$, the real-valued functions on $X$, that satisfies the closure
conditions of the set ${\mathrm{Bic}({\mathbb{R}})}$ of Bishop-continuous
functions from ${\mathbb{R}}$ to ${\mathbb{R}}$. Bishop called $F$ a topology
(of functions) on $X$. The set ${\mathrm{Bic}({\mathbb{R}})}$ of Bishop-
continuous functions $\phi:{\mathbb{R}}\to{\mathbb{R}}$ is the canonical
topology of functions on ${\mathbb{R}}$. Bishop also defined
inductively111This definition, together with the notion of the least algebra
of Borel sets generated by a family of complemented subsets of $X$, relative
to a given set of real-valued functions on $X$, are the main inductive
definitions found in [3], both in chapter 3. The notion of the least algebra
of Borel sets is avoided in [4] and [5], and the notion of the least topology
is not developed neither in [3] nor in [5]. the least topology of functions on
$X$ that includes a given subset $F_{0}$ of $\mathbb{F}(X)$. The concept of
function space was proposed as a function-theoretic alternative to the notion
of topological space.

In [5], p. 77, Bishop and Bridges expressed in a clear way the superiority of
the function-theoretic notion of function space to the set-theoretic notion of
neighborhood space. As Bridges and Palmgren remark in [9], “little appears to
have been done” in the theory of neighborhood spaces. Ishihara has worked in
[18] (and with co-authors in [17]) on their connections to the apartness
spaces of Bridges and Vîţă (see [8]), and in [19] on their connections to
Bishop’s function spaces, while in [20] Ishihara and Palmgren studied the
notion of quotient topology in neighborhood spaces.

Bridges talked on Bishop’s function spaces at the first workshop on formal
topology in 1997, and revived the subject of function spaces in [11].
Motivated by Bridges’s paper, Ishihara showed in [19] the existence of an
adjunction between the category of neighbourhood spaces and the category of
$\Phi$-closed pre-function spaces, where a pre-function space is an extension
of the notion of a function space. In [27]-[35] we try to develop the theory
of function spaces, or Bishop spaces, as we call them. In [33] and in [32] we
also study the applications of the theory of set-indexed families of Bishop
sets in the theory of Bishop spaces. In [15] connections between the theory of
Bishop spaces and the theory of $C$-spaces of Escardó and Xu, developed in
[43] and in [14], are studied.

A group $X$ is a topological group, if there is a topology of open sets
$\mathcal{T}$ on $X$ such that the corresponding operations $+\colon X\times
X\to X$ and $-\colon X\to X$ are continuous functions with respect to
$\mathcal{T}$. The theory of topological groups is very well-developed, with
numerous applications (see [2], [16] and [42]). We call a group $X$, equipped
with a Bishop topology of functions $F$, a Bishop topological group, if the
corresponding group operations $+\colon X\times X\to X$ and $-\colon X\to X$
are Bishop morphisms with respect to $F$. A Bishop morphism between Bishop
spaces is the notion of arrow in the category of Bishop spaces that was
introduced by Bridges in [11] and corresponds to the notion of a continuous
function between topological spaces.

Most of the concepts of the theory of Bishop spaces are function-theoretic
i.e., they are determined by the Bishop topology of functions $F$ on $X$. Each
Bishop topology $F$ generates a canonical neighborhood structure, a family of
basic open sets in $X$, described in section 3. As explained above, a closed
set $C$ with respect to this neighborhood structure is defined positively, and
independently from its set-theoretic complement. Generally we cannot show
constructively that the set-theoretic complement $X\setminus C$ of a closed
set $C$ is open. What we show in Theorem 3.2 though, is that a positive notion
of complement, determined by $F$, the $F$-complement $X\setminus_{F}C$ of $C$,
is the largest open set included in $X\setminus C$.

In the main core of this paper we prove some fundamental properties of the
closed sets in Bishop topological groups. Using functions to describe general
properties of sets, and working with the aforementioned positive notion of
closed set gives us the opportunity to find constructive proofs with a clear
computational content of results, which in many cases in the classical theory
of topological groups depend on the use of classical negation. Moreover, our
concepts and results avoid the use even of countable choice (CC). Although
practicioners of Bishop-style constructive mathematics usually embrace CC,
avoiding it, and using non-sequential or non-choice-based arguments instead,
forces us to formulate “better” concepts and find “better” proofs. This
standpoint was advocated first by Richman (see [37] and [41]).

The study of closed sets in the neighborhood structure induced by the Bishop
topology of a Bishop topological group shows the fruitfulness of combining the
two constructive proposals of Bishop to the classical topology of open sets.
Moreover, the group-structure of a Bishop space $X$ helps us “recover” part of
the classical duality between closed and open sets. As Corollary 5.10
indicates, there are many cases of closed sets in a Bishop topological group
for which we can show that their set-theoretic complement is open!

The structure of this paper is the following:

  * •

In section 2 we include all definitions and facts on Bishop spaces that are
necessary to the rest of the paper. All proofs not given here are found in
[28]. For all results on constructive analysis that are used here without
proof, we refer to [5].

  * •

In section 3 we give all definitions and results on the canonical neighborhood
structure of a Bishop topology that are used here. Theorem 3.2 is the result
of this section that is most relevant to the study of closed sets in Bishop
topological groups.

  * •

In section 4 we introduce Bishop topological groups and we prove some of their
fundamental properties.

  * •

In section 5, the central section of our paper, we prove fundamental
properties of closed sets in Bishop topological groups. As we work with
functions and positively defined concepts, avoiding the use of choice, our
proofs generate clear algorithms. For all algebraic notions within
$\mathrm{BISH}$ used here, we refer to [24].

We work within Bishop’s informal system of constructive mathematics
$\mathrm{BISH}$, without countable choice, equipped with inductive definitions
with rules of countably many premises. A set-theoretic formal framework for
this system222Extensional Martin-Löf Type Theory or the theory of setoids
within intensional Martin-Löf Type Theory are possible type-theoretic systems
for this informal system (see [12]), although there choice, in the form of the
distributivity of $\prod$ over $\sum$, is provable. is Myhill’s
$\mathrm{CST}^{*}$ without countable choice, or $\mathrm{CZF}$, equipped with
a weak form of Aczel’s regular extension axiom $\mathrm{REA}$ (see [1] and
[26]).

##  2 Fundamentals of Bishop spaces

If $a,b\in{\mathbb{R}}$, let $a\vee b:=\max\\{a,b\\}$ and $a\wedge
b:=\min\\{a,b\\}$. Hence, $|a|=a\vee(-a)$. If $f,g\in\mathbb{F}(X)$, let
$f=_{\mathbb{F}(X)}g:\Leftrightarrow\forall_{x\in
X}\big{(}f(x)=_{{\mathbb{R}}}f(y)\big{)}$. If $f,g\in\mathbb{F}(X)$,
$\varepsilon>0$ and $\Phi\subseteq\mathbb{F}(X)$, let

$U(g,f,\varepsilon):\Leftrightarrow\forall_{x\in
X}\big{(}|g(x)-f(x)|\leq\varepsilon\big{)},$
$U(\Phi,f):\Leftrightarrow\forall_{\varepsilon>0}\exists_{g\in\Phi}\big{(}U(g,f,\varepsilon)\big{)}.$

A set $X$ is inhabited, if it has an element. We denote by $\overline{a}^{X}$,
or simply by $a$, the constant function on $X$ with value $a\in{\mathbb{R}}$,
and by $\mathrm{Const}(X)$ their set.

######  Definition 2.1.

A Bishop space is a pair $\mathcal{F}:=(X,F)$, where $X$ is an inhabited set
and $F$ is an extensional subset of $\mathbb{F}(X)$ i.e.,
$\forall_{f,g\in\mathbb{F}(X)}\big{(}[f\in F\ \&\
g=_{\mathbb{F}(X)}f]\Rightarrow g\in F\big{)}$, such that the following
conditions hold:
$(\mathrm{BS}_{1})$ $\mathrm{Const}(X)\subseteq F$.
$(\mathrm{BS}_{2})$ If $f,g\in F$, then $f+g\in F$.
$(\mathrm{BS}_{3})$ If $f\in F$ and $\phi\in\mathrm{Bic}({\mathbb{R}})$, then
$\phi\circ f\in F$.
$(\mathrm{BS}_{4})$ If $f\in\mathbb{F}(X)$ and $U(F,f)$, then $f\in F$.
We call $F$ a Bishop topology on $X$. If $\mathcal{G}:=(Y,G)$ is a Bishop
space, a Bishop morphism from $\mathcal{F}$ to $\mathcal{G}$ is a function
$h:X\to Y$ such that $\forall_{g\in G}\big{(}g\circ h\in F\big{)}$. We denote
by $\mathrm{Mor}(\mathcal{F},\mathcal{G})$ the set of Bishop morphisms from
$\mathcal{F}$ to $\mathcal{G}$. If
$h\in\mathrm{Mor}(\mathcal{F},\mathcal{G})$, we say that $h$ is open, if
$\forall_{f\in F}\exists_{g\in G}\big{(}f=g\circ h\big{)}$. If
$h\in\mathrm{Mor}(\mathcal{F},\mathcal{G})$ is a bijection and $h^{-1}$ is a
Bishop morphism, we call $h$ a Bishop isomorphism.

A Bishop morphism $h\in\mathrm{Mor}(\mathcal{F},\mathcal{G})$ is a
“continuous” function from $\mathcal{F}$ to $\mathcal{G}$. If
$h\in\mathrm{Mor}(\mathcal{F},\mathcal{G})$ is a bijection, then
$h^{-1}\in\mathrm{Mor}(\mathcal{G},\mathcal{F})$ if and only if $h$ is open.
Let $\mathcal{R}$ be the Bishop space of reals
$({\mathbb{R}},{\mathrm{Bic}({\mathbb{R}})})$. It is easy to show that if $F$
is a topology on $X$, then $F=\mathrm{Mor}(\mathcal{F},\mathcal{R})$ i.e., an
element of $F$ is a real-valued “continuous” function on $X$. A Bishop
topology $F$ on $X$ is an algebra and a lattice, where $f\vee g$ and $f\wedge
g$ are defined pointwise, and $\mathrm{Const}(X)\subseteq
F\subseteq\mathbb{F}(X)$. If $\mathbb{F}^{*}(X)$ denotes the bounded elements
of $\mathbb{F}(X)$, then $F^{*}:=F\cap\mathbb{F}^{*}(X)$ is a Bishop topology
on $X$. If $x=_{X}y$ is the given equality on $X$, a Bishop topology $F$ on
$X$ separates the points of $X$, or $F$ is separating (see [27]), if

$\forall_{x,y\in X}\big{[}\forall_{f\in
F}\big{(}f(x)=_{{\mathbb{R}}}f(y)\big{)}\Rightarrow x=_{X}y\big{]}.$

The canonical apartness relation on $X$ induced by $F$ is defined by

$x\neq_{F}y:\Leftrightarrow\exists_{f\in
F}\big{(}f(x)\neq_{{\mathbb{R}}}f(y)\big{)}.$

An apartness relation on $X$ is a positively defined inequality on $X$. E.g.,
if $a,b\in{\mathbb{R}}$, then $a\neq_{{\mathbb{R}}}b:\Leftrightarrow|a-b|>0$.
In Proposition 5.1.2. of [28] we show that
$a\neq_{{\mathbb{R}}}b\Leftrightarrow a\neq_{{\mathrm{Bic}({\mathbb{R}})}}b$.

######  Definition 2.2.

Turning the definitional clauses $(\mathrm{BS}_{1})-(\mathrm{BS}_{4})$ into
inductive rules, the least topology $\bigvee F_{0}$ generated by a set
$F_{0}\subseteq\mathbb{F}(X)$, called a subbase of $\bigvee F_{0}$, is defined
by the following inductive rules:

$\frac{f_{0}\in F_{0}}{f_{0}\in\bigvee F_{0}},\ \ \ \frac{f\in\bigvee F_{0},\
g\in\mathbb{F}(X),\ g=_{\mathbb{F}(X)}f}{g\in\bigvee F_{0}},\ \ \
\frac{a\in{\mathbb{R}}}{\overline{a}\in\bigvee F_{0}},\ \ \
\frac{f,g\in\bigvee F_{0}}{f+g\in\bigvee F_{0}},$
$\displaystyle\begin{aligned} f\in\bigvee F_{0}g_{1}\in\bigvee F_{0}\ \&\
U(g_{1},f,\frac{1}{2}),\ g_{2}\in\bigvee F_{0}\ \&\
U(g_{2},f,\frac{1}{2^{2}}),\ g_{3}\in\bigvee F_{0}\ \&\
U(g_{3},f,\frac{1}{2^{3}}),\ldots\end{aligned}.$

The above rules induce the corresponding induction principle
$\mathrm{Ind}_{\bigvee F_{0}}$ on $\bigvee F_{0}$.

If $h\colon X\to Y$ and $G=\bigvee G_{0}$, then one can show inductively i.e.,
with the use of $\mathrm{Ind}_{\bigvee G_{0}}$, that
$h\in\mathrm{Mor}(\mathcal{F},\mathcal{G})\Leftrightarrow\forall_{g_{0}\in
G_{0}}\big{(}g_{0}\circ h\in F\big{)}$. We call this property the
$\bigvee$-lifting of morphisms.

######  Definition 2.3.

If $\mathcal{F}=(X,F)$ and $\mathcal{G}=(Y,G)$ are given Bishop spaces, their
product is the structure $\mathcal{F}\times\mathcal{G}=(X\times Y,F\times G)$,
where

$F\times G:=\bigvee\\{f\circ\pi_{1}\mid f\in F\\}\cup\\{g\circ\pi_{2}\mid g\in
G\\}:=\bigvee_{f\in F}^{g\in G}f\circ\pi_{1},g\circ\pi_{2},$

and $\pi_{1},\pi_{2}$ are the projections of $X\times Y$ to $X$ and $Y$,
respectively.

It is straightforward to show that $\mathcal{F}\times\mathcal{G}$ satisfies
the universal property for products and that $F\times G$ is the least topology
which turns the projections $\pi_{1},\pi_{2}$ into morphisms. If $F_{0}$ is a
subbase of $F$ and $G_{0}$ is a subbase of $G$, then we show inductively that

$\bigvee F_{0}\times\bigvee G_{0}=\bigvee\\{f_{0}\circ\pi_{1}\mid f_{0}\in
F_{0}\\}\cup\\{g_{0}\circ\pi_{2}\mid g_{0}\in G_{0}\\}:=\bigvee_{f_{0}\in
F_{0}}^{g_{0}\in G_{0}}f_{0}\circ\pi_{1},g_{0}\circ\pi_{2}.$

Consequently,
$\mathrm{Bic}(\mathbb{R})\times\mathrm{Bic}(\mathbb{R})=\bigvee\mathrm{id}_{\mathbb{R}}\circ\pi_{1},\mathrm{id}_{\mathbb{R}}\circ\pi_{2}=\bigvee\pi_{1},\pi_{2}$.

######  Corollary 2.4.

Let $\mathcal{H}=(Z,H),\mathcal{F}=(X,F),\mathcal{G}=(Y,G)$ be Bishop spaces.
(i) If $h_{1}:Z\rightarrow X$, $h_{2}:Z\rightarrow Y$, the map $h_{1}\times
h_{2}:Z\rightarrow X\times Y,$ defined by $z\mapsto(h_{1}(z),h_{2}(z)),$ is in
$\mathrm{Mor}(\mathcal{H},\mathcal{F}\times\mathcal{G})$ if and only if
$h_{1}\in\mathrm{Mor}(\mathcal{H},\mathcal{F})$ and
$h_{2}\in\mathrm{Mor}(\mathcal{H},\mathcal{G})$.
(ii) If $e_{1}:X\rightarrow Z$, $e_{2}:Y\rightarrow Z$, then the map
$e_{1}\otimes e_{2}:X\times Y\rightarrow Z\times Z,$ defined by
$(x,y)\mapsto(e_{1}(x),e_{2}(y)),$ is in
$\mathrm{Mor}(\mathcal{F}\times\mathcal{G},\mathcal{H}\times\mathcal{H})$ if
and only if $e_{1}\in\mathrm{Mor}(\mathcal{F},\mathcal{H})$ and
$e_{2}\in\mathrm{Mor}(\mathcal{G},\mathcal{H})$.

######  Proposition 2.5.

Suppose that $\mathcal{F}=(X,F)$, $\mathcal{G}=(Y,G)$, $\mathcal{H}=(Z,H)$ are
Bishop spaces, $x\in X,y\in Y$, $\phi:X\times Y\rightarrow\mathbb{R}\in
F\times G$ and $\Phi:X\times Y\rightarrow
Z\in\mathrm{Mor}(\mathcal{F}\times\mathcal{G},\mathcal{H})$.
(i) $i_{x}:Y\rightarrow X\times Y$, $y\mapsto(x,y)$, and $i_{y}:X\rightarrow
X\times Y$, $x\mapsto(x,y)$, are open morphisms.
(ii) $\phi_{x}:Y\rightarrow\mathbb{R}$, $y\mapsto\phi(x,y)$, and
$\phi_{y}:X\rightarrow\mathbb{R}$, $x\mapsto\phi(x,y)$, are in $G$ and $F$,
respectively.
(iii) $\Phi_{x}:Y\rightarrow Z$, $y\mapsto\Phi(x,y)$, and
$\Phi_{y}:X\rightarrow Z$, $x\mapsto\Phi(x,y)$, are in
$\mathrm{Mor}(\mathcal{G},\mathcal{H})$ and
$\mathrm{Mor}(\mathcal{F},\mathcal{H})$, respectively.

###### Proof.

(i) We show it only for $i_{y}$. By the ${\mathcal{F}}$-lifting of morphisms
we have that
$i_{y}\in\mathrm{Mor}(\mathcal{F},\mathcal{F}\times\mathcal{G})\Leftrightarrow\forall_{f\in
F}((f\circ\pi_{1})\circ i_{y}\in F)\ \&\ \forall_{g\in G}((g\circ\pi_{2})\circ
i_{y}\in F)$. If $f\in F$, then $(f\circ\pi_{1})\circ i_{y}=f$, which shows
also that $i_{y}$ is open, while if $g\in G$, then $(g\circ\pi_{2})\circ
i_{y}=\overline{g(y)}\in F$.
(ii) We show it only for $\phi_{y}$. We have that $\phi_{y}=\phi\circ i_{y}$,
since $(\phi\circ i_{y})(x)=\phi(x,y)=\phi_{y}(x)$, for each $x\in X$. Since
$i_{y}\in\mathrm{Mor}(\mathcal{F},\mathcal{F}\times\mathcal{G})$ and $\phi\in
F\times G$, we get that $\phi\circ i_{y}=\phi_{y}\in F$.
(iii) The proof is similar to the proof of (ii), Actually, (ii) is a special
case of (iii). ∎

##  3 The neighborhood structure of a Bishop topology

If $F$ is a Bishop topology on $X$, the neighborhood structure on $X$ induced
by $F$ is the family $(U(f)_{f\in F}$, where $U(f):=\\{x\in X\mid f(x)>0\\}$.
The covering condition $(\mathrm{NS}_{1})$ follows from the equality
$U(\overline{\alpha}^{X})=X$, where $a>0$, and the neighborhood-condition
$(\mathrm{NS}_{2})$ follows from the equality $U(f)\cap U(g)=U(f\wedge g)$,
for every $f,g\in F$. Consequently, $O\subseteq X$ is open if

$\forall_{x\in O}\exists_{f\in F}\big{(}f(x)>0\ \&\ U(f)\subseteq O\big{)},$

and $C\subseteq X$ is closed, if $\forall_{x\in
X}\big{(}x\in\overline{C}\Rightarrow x\in C\big{)}$, where

$x\in\overline{C}:\Leftrightarrow\forall_{f\in
F}\big{(}f(x)>0\Rightarrow\exists_{c\in C}\big{(}f(c)>0\big{)}\big{)}.$

######  Proposition 3.1.

Let $\mathcal{F}=(X,F)$, $\mathcal{G}=(Y,G)$ be Bishop spaces, $f\in F$ and
$h:X\rightarrow Y$.
(i) $\mathcal{O}$ is open in $N(\mathrm{Bic}({\mathbb{R}}))$ if and only if it
is open in the standard topology on ${\mathbb{R}}$.
(ii) If $h\in\mathrm{Mor}(\mathcal{F},\mathcal{G})$, then $h$ is neighborhood-
continuous.
(iii) If $h\in\mathrm{Mor}(\mathcal{F},\mathcal{G})$, the inverse image of a
closed set in $Y$ under $h$ is closed in $X$.
(iv) If $h\in\mathrm{Mor}(\mathcal{F},\mathcal{G})$ and $A\subseteq X$, then
$h(\overline{A})\subseteq\overline{h(A)}$.
(v) The set-theoretic complement $X\setminus U(f)$ of $U(f)$ in $X$ is closed
in $X$, for every $f\in F$.
(vi) The zero set $\zeta(f):=\\{x\in X\mid f(x)=0\\}$ is closed.

###### Proof.

For (i)-(v) see [28], Proposition 4.4, and for (vi) see [28], Proposition
5.3.2. ∎

Clearly, $C\subseteq X$ is closed if and only if $C=\overline{C}$, and the
intersection of closed sets is closed. The closure operator
$A\mapsto\overline{A}$ is not topological, in the classical sense, as we
cannot show constructively that the union of two closed sets is closed, in
general,closed (see also [5], p. 79). If $A,B\subseteq X$ and $F$ a Bishop
topology on $X$, then it is straightforward to show that (i)
$A\subseteq\overline{A}$, (ii) $\overline{\overline{A}}\subseteq\overline{A}$,
(iii) $A\subseteq B\Rightarrow\overline{A}\subseteq\overline{B}$, and (iv)
$\overline{A}\cup\overline{B}\subseteq\overline{A\cup B}$. The inverse
inclusion $\overline{A\cup B}\subseteq\overline{A}\cup\overline{B}$ cannot be
shown constructively. If $F$ is a Bishop topology on $X$ and $C\subseteq X$,
we define positively and through $F$ a stronger relation “$x$ is not in $C$”,
where $x\in X$, by

$x\notin_{F}C:\Leftrightarrow\exists_{f\in F}\big{(}f\colon
x\notin_{F}C\big{)},$ $f\colon x\notin_{F}C:\Leftrightarrow f(x)>0\ \&\
\forall_{c\in C}\big{(}f(c)=0\big{)}.$

Classically one can show that $F$ is always completely regular i.e., if $C$ is
closed in $X$ and $x\notin C$, then $x\notin_{F}C$ (see [28], Proposition
3.7.6). Constructively we can show the following.

######  Theorem 3.2.

Let $F$ be a Bishop topology on $X$ and $C$ closed in $X$. The $F$-complement
$X\setminus_{F}C:=\\{x\in X\mid\exists_{f\in F}\big{(}f\colon x\notin_{F}C\\}$
of $C$ in $X$ is the largest open set included in $X\setminus C$.

###### Proof.

We show that $X\setminus_{F}C$ is an open set included in $X\setminus C$ and
if $O$ is an open set included in $X\setminus C$, then $O\subseteq
X\setminus_{F}C$. First we show that $X\setminus_{F}C$ is open. If $x\in
X\setminus_{F}C$, let $f\in F$ such that $f\colon x\notin_{F}C$. Clearly,
$x\in U(f)$, and if $y\in X$ such that $y\in U(f)$, then $f\colon
y\notin_{F}C$ i.e., $y\in X\setminus_{F}C$. Next we show that if $x\in
X\setminus_{F}C$, then $x\in X\setminus C$. If $x\in C$, then $f(x)>0$ and
$f(x)=0$, which is a contradiction. Suppose next that $O$ is an open set
included in $X\setminus C$. We show that if $x\in O$, then $x\in
X\setminus_{F}C$. Since $O$ is open, there is $g\in F$ such that $g(x)>0$ and
$U(g)\subseteq O\subseteq X\setminus C$. We have that $g(c)\leq 0$, for every
$c\in C$, since if $g(c)>0$, for some $c\in C$, then $c\in U(g)$, hence $c\in
X\setminus C$, which is a contradiction. By the constructively valid
implication $\neg(a>0)\Rightarrow a\leq 0$, for every $a\in{\mathbb{R}}$ (see
[5], Lemma 2.18), we get $g(c)\leq 0$. Since $g\vee\overline{0}^{X}\in F$, we
conclude that $g\vee\overline{0}^{X}\colon x\notin_{F}C$, hence $x\in
X\setminus_{F}C$. ∎

Although we cannot show in general that $X\setminus C$ is open, and hence
$X\setminus C=X\setminus_{F}C$, we can replace this computationally dubious
result by the computationally meaningful fact that $X\setminus_{F}C$ is the
largest open set included in $X\setminus C$. The next result is used in the
proofs of Theorem 5.6(ii) and Theorem 5.7(ii).

######  Proposition 3.3.

If $F$ is a Bishop topology on $X$, the following are equivalent:
(i) $F$ separates the points of $X$.
(ii) The inequality $\neq_{F}$ generated by $F$ is tight i.e.,
$\neg(x\neq_{F}y)\Rightarrow x=_{X}y$, for every $x,y\in X$.
(iii) The singleton $\\{x\\}$ is closed, for every $x\in X$.

###### Proof.

(i)$\Rightarrow$(ii) Let $\neg(x=_{F}y):\Leftrightarrow\neg[\exists_{f\in
F}\big{(}f(x)\neq_{{\mathbb{R}}}f(y)\big{)}]$, for some $x,y\in X$. We show
that $\forall_{f\in F}\big{(}f(x)=_{{\mathbb{R}}}f(y)\big{)}$. Let $f\in F$
such that $f(x)\neq_{{\mathbb{R}}}f(y)$. By our hypothesis on $x,y$ this is
impossible, hence by the tightness of $\neq_{{\mathbb{R}}}$ we conclude that
$f(x)=_{{\mathbb{R}}}f(y)$.
(ii)$\Rightarrow$(iii) Let $x,y\in X$ such that $\forall_{f\in
F}\big{(}f(y)>0\Rightarrow f(x)>0\big{)}$. We show that $y=_{X}x$, by showing
that $\neg\big{(}y\neq_{F}x\big{)}$. Suppose that $y\neq_{F}x$ and, without
loss of generality, let $g\in F$ such that $g(y)=1$ and $g(x)=0$. By the
hypothesis on $x$ we have that $g(y)>0\Rightarrow g(x)>0$, and we get the
required contradiction.
(iii)$\Rightarrow$(i) Let $x,y\in X$ such that $\forall_{f\in
F}\big{(}f(x)=_{{\mathbb{R}}}f(y)\big{)}$. We show that
$y\in\overline{\\{x\\}}$, hence $y=x$. Let $f\in F$ such that $f(y)>0$. Since
$f(x)=f(y)$, we get $f(x)>0$. ∎

######  Proposition 3.4.

If $C$ is closed in $X$ and $D\subseteq Y$ is closed in $Y$, $C\times D$ is
closed in $X\times Y$.

###### Proof.

Let $(x,y)\in\overline{C\times D}$ i.e., if $h(x,y)>0$, there is $(u,w)\in
C\times D$ such that $h(u,w)>0$, for every $h\in F\times G$. We show that
$x\in\overline{C}$ and (similarly) $y\in\overline{D}$, hence $(x,y)\in C\times
D$. Let $f\in F$ such that $f(x)>0$. Since $(f\circ\pi_{1})(x,y)>0$ and
$f\circ\pi_{1}\in F\times G$, there is $(u,w)\in C\times D$ such that
$(f\circ\pi_{1})(u,w):=f(u)>0$, hence there is $u\in C$ with $f(u)>0$. ∎

##  4 Bishop topological groups

######  Definition 4.1.

A Bishop topological group is a structure
$\boldsymbol{\mathcal{F}}:=(X,+,0,-;F)$, where $\mathcal{X}:=(X,+,0,-)$ is a
group and $\mathcal{F}:=(X,F)$ is a Bishop space such that $+:X\times X\to
X\in\mathrm{Mor}(\mathcal{F}\times\mathcal{F},\mathcal{F})$ and $-:X\to
X\in\mathrm{Mor}(\mathcal{F},\mathcal{F})$. If necessary, we also use the
notations $+^{{X}},0^{{X}}$, and $-^{{X}}$ for the operations of the group
$\mathcal{X}$. If $f\in F$, let $f_{+}:=f\circ+$ and $f_{-}:=f\circ-$.

By the definition of a Bishop morphism we get

$+\in\mathrm{Mor}(\mathcal{F}\times\mathcal{F},\mathcal{F}):\Leftrightarrow\forall_{f\in
F}\big{(}f\circ+\in F\times F\big{)}:\Leftrightarrow\forall_{f\in
F}\big{(}f_{+}\in F\times F\big{)},$
$-\in\mathrm{Mor}(\mathcal{F},\mathcal{F}):\Leftrightarrow\forall_{f\in
F}\big{(}f\circ-\in F\big{)}:\Leftrightarrow\forall_{f\in F}\big{(}f_{-}\in
F\big{)}.$

######  Example 4.2 (The additive group of reals).

The structure
$\boldsymbol{\mathcal{R}}:=({\mathbb{R}},+,0,-;{\mathrm{Bic}({\mathbb{R}})})$
is a Bishop topological group. By the $\bigvee$-lifting of morphisms
$+\in\mathrm{Mor}(\mathcal{R}\times\mathcal{R},\mathcal{R})\Leftrightarrow\mathrm{id}_{{\mathbb{R}}}\circ+\in{\mathrm{Bic}({\mathbb{R}})}\times{\mathrm{Bic}({\mathbb{R}})}.$
If $x,y\in{\mathbb{R}}$, then
$\big{(}\mathrm{id}_{{\mathbb{R}}}\circ+\big{)}(x,y):=x+y:=(\pi_{1}+\pi_{2})(x,y)$
i.e.,
$\mathrm{id}_{{\mathbb{R}}}\circ+=\pi_{1}+\pi_{2}\in{\mathrm{Bic}({\mathbb{R}})}\times{\mathrm{Bic}({\mathbb{R}})}=\bigvee\pi_{1},\pi_{2}$.
Similarly,
$-\in\mathrm{Mor}(\mathcal{R},\mathcal{R})\Leftrightarrow\mathrm{id}_{{\mathbb{R}}}\circ-\in{\mathrm{Bic}({\mathbb{R}})}$.
If $x\in{\mathbb{R}}$, then
$\big{(}\mathrm{id}_{{\mathbb{R}}}\circ-\big{)}(x):=-x:=-\mathrm{id}_{{\mathbb{R}}}(x)$
i.e.,
$\mathrm{id}_{{\mathbb{R}}}\circ-=-\mathrm{id}_{{\mathbb{R}}}\in{\mathrm{Bic}({\mathbb{R}})}$.

######  Example 4.3 (The trivial Bishop topological group).

If $\mathcal{X}:=(X,+,0,-)$ is a group, then $\mathrm{Const}(X)$ is the
trivial Bishop topology on $X$. If $a\in{\mathbb{R}}$, then
$\overline{a}^{X}\circ+=\overline{a}^{X\times X}\in\mathrm{Const}(X\times
X)=\mathrm{Const}(X)\times\mathrm{Const}(X)$, and
$\overline{a}^{X}\circ-=\overline{a}^{X}\in\mathrm{Const}(X)$.

Unless otherwise stated, from now on, $X,Y$ are Bishop topological groups with
$F$ and $G$ Bishop topologies on $X$ and $Y$, respectively.

######  Proposition 4.4.

(i) The function $-:X\to X$ is a Bishop isomorphism.
(ii) For every $x_{0}\in X$ the functions $+_{x_{0}}^{1},+_{x_{0}}^{2}:X\to
X$, defined by $+_{x_{0}}^{1}(x):=x_{0}+x$ and $+_{x_{0}}^{2}(x):=x+x_{0},$
for every $x\in X$, are Bishop morphisms.
(iii) If $f\in F$, the functions
$f_{x_{0}}^{1},f_{x_{0}}^{2}:X\to{\mathbb{R}}$, defined by
$f_{x_{0}}^{1}(x):=f(x_{0}+x)$ and $f_{x_{0}}^{2}(x):=f(x+x_{0}),$ for every
$x\in X$, are in $F$.
(iv) For every $x_{0}\in X$ the functions $+_{x_{0}}^{1},+_{x_{0}}^{2}:X\to X$
are Bishop isomorphisms.

###### Proof.

(i) By definition $-\in\mathrm{Mor}(\mathcal{F},\mathcal{F})$, and it is a
bijection. It is also open i.e., $\forall_{f\in F}\exists_{g\in
F}\big{(}f=g_{-}\big{)}$. If $f\in F$, we have that $f=(f_{-})_{-}$ and
$f_{-}\in F$.
(ii) and (iii) If $i_{x_{0}}^{1}:X\to X\times X$ is defined by
$i_{x_{0}}^{1}(x):=(x_{0},x)$, for every $x\in X$, then
$i_{x_{0}}^{1}\in\mathrm{Mor}(\mathcal{F},\mathcal{F}\times\mathcal{F})$ and
$+_{x_{0}}^{1}:=+\circ i_{x_{0}}^{1}\in\mathrm{Mor}(\mathcal{F},\mathcal{F})$
as a composition of Bishop morphisms

$X$$X\times X$$X$${\mathbb{R}}$.$\ \ \ \ \ {i_{x_{0}}^{1}}$$+$${f}\ \
$$+_{x_{0}}^{1}$$f_{x_{0}}^{1}$

$f_{x_{0}}^{1}=f\circ+_{x_{0}}^{1}\in F$, as a composition of Bishop
morphisms. For $+_{x_{0}}^{2}$ we work similarly.
(iv) Clearly, $+_{x_{0}}^{1}$ is a bijection. It is also open, since for every
$f\in F$ we have that $f=f_{-x_{0}}^{1}\circ+_{x_{0}}^{1},$ and by (iv)
$f_{-x_{0}}^{1}\in F$. For $f_{x_{0}}^{2}$ we work similarly. ∎

######  Proposition 4.5.

The function $k:X\times X\to X\times X$, defined by $k(x,y):=(x,-y)$, for
every $(x,y)\in X\times X$, is a Bishop isomorphism.

###### Proof.

Clearly, $k$ is a bijection. By the $\bigvee$-lifting of morphisms we have
that
$k\in\mathrm{Mor}(\mathcal{F}\times\mathcal{F},\mathcal{F}\times\mathcal{F})$
if and only if $(f\circ\pi_{1})\circ k\in F\times F$ and $(f\circ\pi_{2})\circ
k\in F\times F\big{)}$, for every $f\in F$. Let $f\in F$ and $(x,y)\in X\times
X$. Since $[(f\circ\pi_{1})\circ
k](x,y):=(f\circ\pi_{1})(x,-y):=f(x):=(f\circ\pi_{1})(x,y),$ we get
$(f\circ\pi_{1})\circ k=f\circ\pi_{1}\in F\times F$. Moreover,
$[(f\circ\pi_{2})\circ
k](x,y):=(f\circ\pi_{2})(x,-y):=f(-y):=f_{-}(y):=(f_{-}\circ\pi_{2})(x,y),$
i.e., $(f\circ\pi_{2})\circ k=(f_{-}\circ\pi_{2})\in F\times F$, since
$f_{-}\in F$. Since $(k\circ k)(x,y):=(x,-(-y))=(x,y)$, $k$ is its own
inverse, hence $k$ is a Bishop isomorphism. ∎

######  Proposition 4.6.

Let $\mathcal{X}:=(X,+,0,-)$ be a group, $F$ a Bishop topology on $X$, and
$\textnormal{{sub}}:X\times X\to X$ be defined by
$\textnormal{{sub}}(x,y):=x-y,$ for every $(x,y)\in X\times X$. Then
$\boldsymbol{\mathcal{F}}:=(X,+,0,-;F)$ is a Bishop topological group if and
only if
$\textnormal{{sub}}\in\mathrm{Mor}(\mathcal{F}\times\mathcal{F},\mathcal{F})$.

###### Proof.

If $\boldsymbol{\mathcal{F}}$ is a Bishop topological group, then
$\textnormal{{sub}}=+\circ
k\in\mathrm{Mor}(\mathcal{F}\times\mathcal{F},\mathcal{F})$

$X\times X$$X\times X$$X$$X$.$k$$+$subsub$+$

For the converse, notice that $+=\textnormal{{sub}}\circ
k\in\mathrm{Mor}(\mathcal{F}\times\mathcal{F},\mathcal{F})$. By Proposition
2.5(iii) we get
$-=\textnormal{{sub}}_{0}\in\mathrm{Mor}(\mathcal{F},\mathcal{F})$, where
$\textnormal{{sub}}_{0}(y):=\textnormal{{sub}}(0,y):=-y$, for every $y\in X$.
∎

######  Proposition 4.7.

Let $\boldsymbol{\mathcal{F}}:=(X,+,0,-;F)$ be a Bishop topological group and
$\mathcal{G}:=(Y,G)$ a Bishop space. Let the functions
$+^{{{\to}}}:\mathrm{Mor}(\mathcal{G},\mathcal{F})\times\mathrm{Mor}(\mathcal{G},\mathcal{F})\to\mathrm{Mor}(\mathcal{G},\mathcal{F})$,
$-^{{{\to}}}:\mathrm{Mor}(\mathcal{G},\mathcal{F})\to\mathrm{Mor}(\mathcal{G},\mathcal{F})$,
and $0^{{\to}}:Y\to X$ be defined by
$(h_{1}+^{{\to}}h_{2})(y):=h_{1}(y)+h_{2}(y)$, $(-^{{\to}}h)(y):=-h(y)$, and
$0^{{\to}}(y):=0$, for every $y\in Y$, and
$h_{1},h_{2},h\in\mathrm{Mor}(\mathcal{G},\mathcal{F})$. Then
$\big{(}\mathrm{Mor}(\mathcal{G},\mathcal{F}),+^{{\to}},0^{{\to}},-^{{\to}}\big{)}$
is a group.

One can show that the group
$\big{(}\mathrm{Mor}(\mathcal{G},\mathcal{F}),+^{{\to}},0^{{\to}},-^{{\to}}\big{)}$,
equipped with the pointwise exponential Bishop topology (see [28], section
4.3), is a Bishop topological group. Notice that if $Y$ has also a group
structure compatible with $G$, and if $h_{1},h_{2},h$ are group homomorphisms,
then $h_{1}+^{{\to}}h_{2},-^{{\to}}h$ and $0^{{\to}}$ are also group
homomorphisms.

######  Definition 4.8.

Let $\boldsymbol{\mathcal{F}}:=(X,+^{{X}},0^{{X}},-^{{X}};F)$ and
$\boldsymbol{\mathcal{G}}:=(Y,+^{{Y}},0^{{Y}},-^{{Y}};G)$ be Bishop
topological groups. If $h\in\mathrm{Mor}(\mathcal{G},\mathcal{F})$ such that
$h$ is a $(\mathcal{X},\mathcal{Y})$-group homomorphism, then we call $h$ a
Bishop group homomorphism, or simpler, a Bishop homomorphism. We denote by
$\textnormal{{Mor}}(\boldsymbol{\mathcal{F}},\boldsymbol{\mathcal{G}})$ the
set of all Bishop homomorphisms from $\boldsymbol{\mathcal{F}}$ to
$\boldsymbol{\mathcal{G}}$. Let BTopGrp be the category of Bishop topological
groups with Bishop group homomorphisms.

######  Proposition 4.9.

Let $a\in{\mathbb{R}}$ and let $h_{a}:{\mathbb{R}}\to{\mathbb{R}}$ be defined
by $h_{a}(x)=ax$, for every $x\in{\mathbb{R}}$. Then
$h_{a}\in\textnormal{{Mor}}(\boldsymbol{\mathcal{R}},\boldsymbol{\mathcal{R}})$.
Conversely, if
$h\in\textnormal{{Mor}}(\boldsymbol{\mathcal{R}},\boldsymbol{\mathcal{R}})$,
there is $a\in{\mathbb{R}}$ such that $h=h_{a}$.

###### Proof.

$h_{a}$ is a group homomorphism, and by the $\bigvee$-lifting of morphisms
$h_{a}\in\mathrm{Mor}(\mathcal{{\mathbb{R}}},\mathcal{{\mathbb{R}}})\Leftrightarrow\mathrm{id}_{{\mathbb{R}}}\circ
h_{a}:=h_{a}\in{\mathrm{Bic}({\mathbb{R}})}$, which holds, since
$h_{a}:=a\cdot\mathrm{id}_{{\mathbb{R}}}\in{\mathrm{Bic}({\mathbb{R}})}$. If
$h\in\textnormal{{Mor}}(\boldsymbol{\mathcal{R}},\boldsymbol{\mathcal{R}})$,
let its restriction $h_{|\mathbb{Q}}$, where
$h_{|\mathbb{Q}}:\mathbb{Q}\to\mathbb{Q}$ is a group homomorphism given by
$\big{(}h_{|\mathbb{Q}}\big{)}(q)=h(1)q$, for every $q\in\mathbb{Q}$. Since
$\mathbb{Q}$ is metrically dense in ${\mathbb{R}}$, by Proposition 4.7.15. in
[28] we have that
$\mathrm{Bic}(\mathbb{Q})={\mathrm{Bic}({\mathbb{R}})}_{|\mathbb{Q}}=\\{\phi_{|\mathbb{Q}}\mid\phi\in{\mathrm{Bic}({\mathbb{R}})}\\}.$
Hence $h_{|\mathbb{Q}}\in\mathrm{Bic}(\mathbb{Q})$. By Lemma 4.7.13. in [28]
there is a unique (up to equality) extension of $h_{|\mathbb{Q}}$ in
${\mathrm{Bic}({\mathbb{R}})}$. Hence $h=h_{h(1)}$. ∎

######  Proposition 4.10.

Let $\boldsymbol{\mathcal{F}}:=(X,+^{{X}},0^{{X}},-^{{X}};F)$ and
$\boldsymbol{\mathcal{G}}:=(Y,+^{{Y}},0^{{Y}},-^{{Y}};G)$ be Bishop
topological groups. Let the functions $+^{{{X\times Y}}}:(X\times
Y)\times(X\times Y)\to X\times Y$, $-^{{{X\times Y}}}:X\times Y\to X\times Y$,
and $0^{{X\times Y}}\in X\times Y$ be defined by $(x,y)+^{{X\times
Y}}(x{{}^{\prime}},y{{}^{\prime}}):=\big{(}x+^{{X}}x{{}^{\prime}},y+^{{Y}}y{{}^{\prime}}\big{)},$
$-^{{X\times Y}}(x,y):=\big{(}-^{{X}}x,-^{{Y}}y\big{)},$ and $0^{{X\times
Y}}:=\big{(}0^{{X}},0^{{Y}}\big{)}$. Then
$\boldsymbol{\mathcal{F}\times\mathcal{G}}:=(X\times Y,+^{{X\times
Y}},0^{{X\times Y}},-^{{X\times Y}};F\times G)$ is a Bishop topological group.

###### Proof.

The proof that $X\times Y$ is a group is omitted as trivial. By the
$\bigvee$-lifting of morphisms $+^{{X\times
Y}}\in\mathrm{Mor}\big{(}[\mathcal{F}\times\mathcal{G}]\times[\mathcal{F}\times\mathcal{G}],\mathcal{F}\times\mathcal{G}\big{)}$
if and only if

$\forall_{f\in F}\forall_{g\in
G}\bigg{(}\big{(}f\circ\pi^{{X}}\big{)}\circ+^{{X\times Y}}\in[F\times
G]\times[F\times G]\&\ \big{(}g\circ\pi^{{Y}}\big{)}\circ+^{{X\times
Y}}\in[F\times G]\times[F\times G]\bigg{)},$

where by the $\bigvee$-lifting of the product Bishop topology

$[F\times G]\times[F\times G]=\bigvee_{f\in F}^{g\in
G}\big{(}f\circ\pi^{{X}}\big{)}\circ\pi_{1}^{{X\times
Y}},\big{(}g\circ\pi^{{Y}}\big{)}\circ\pi_{1}^{{X\times
Y}},\big{(}f\circ\pi^{{X}}\big{)}\circ\pi_{2}^{{X\times
Y}},\big{(}g\circ\pi^{{Y}}\big{)}\circ\pi_{2}^{{X\times Y}}.$

If $f\in F$, $x,x{{}^{\prime}}\in X$, and $y,y{{}^{\prime}}\in Y$, and if
$z:=\big{(}(x,y),(x{{}^{\prime}},y{{}^{\prime}})\big{)}$, then

$\displaystyle\big{[}\big{(}f\circ\pi^{{X}}\big{)}\circ+^{{X\times
Y}}\big{]}\big{(}z\big{)}$
$\displaystyle:=\big{(}f\circ\pi^{{X}}\big{)}\big{(}x+^{{X}}x{{}^{\prime}},y+^{{Y}}y{{}^{\prime}}\big{)}$
$\displaystyle:=f(x+^{{X}}x{{}^{\prime}})$
$\displaystyle:=(f\circ+^{{X}})(x,x{{}^{\prime}})$
$\displaystyle:=(f\circ+^{{X}})\big{(}\pi^{{X}}(x,y),\pi^{{X}}(x{{}^{\prime}},y{{}^{\prime}})\big{)}$
$\displaystyle:=(f\circ+^{{X}})\bigg{(}\big{[}\pi^{{X}}\circ\pi_{1}^{{X\times
Y}}\big{]}\big{(}z\big{)},\big{[}\pi^{{X}}\circ\pi_{2}^{{X\times
Y}}\big{]}\big{(}z\big{)}\bigg{)}$ $\displaystyle:=\big{[}(f\circ+^{{X}})\circ
h\big{)}\big{]}(z),$

where by Corollary 2.4 the function $h:[(X\times Y)\times(X\times Y)]\to
X\times X$, where $h:=\big{[}\pi^{{X}}\circ\pi_{1}^{{X\times
Y}}\big{]}\times\big{[}\pi^{{X}}\circ\pi_{2}^{{X\times Y}}\big{]}$ is a Bishop
morphism. Since $\big{(}f\circ\pi^{{X}}\big{)}\circ+^{{X\times
Y}}=(f\circ+^{{X}})\circ h$

$(X\times Y)\times(X\times Y)$$X\times
X$$X$${\mathbb{R}}$,$h$$+^{{X}}$$f$${\big{(}f\circ\pi^{{X}}\big{)}\circ+^{{X\times
Y}}}$

we get $\big{(}f\circ\pi^{{X}}\big{)}\circ+^{{X\times
Y}}\in\mathrm{Mor}\big{(}[\mathcal{F}\times\mathcal{G}]\times[\mathcal{F}\times\mathcal{G}],\mathcal{R}\big{)}$
as a composition of Bishop morphisms, hence
$\big{(}f\circ\pi^{{X}}\big{)}\circ+^{{X\times Y}}\in[F\times G]\times[F\times
G]$. Working similarly, we get $\big{(}g\circ\pi^{{Y}}\big{)}\circ+^{{X\times
Y}}\in[F\times G]\times[F\times G]$. By the $\bigvee$-lifting of morphisms we
also have that

$-^{{X\times
Y}}\in\mathrm{Mor}\big{(}\mathcal{F}\times\mathcal{G},\mathcal{F}\times\mathcal{G}\big{)}\Leftrightarrow\forall_{f\in
F}\forall_{g\in G}\bigg{(}\big{(}f\circ\pi^{{X}}\big{)}\circ-^{{X\times Y}}\in
F\times G\ \&\ \big{(}g\circ\pi^{{Y}}\big{)}\circ-^{{X\times Y}}\in F\times
G\bigg{)}.$

If $f\in F$, $x\in X$, and $y\in Y$, then

$\big{[}(\big{(}f\circ\pi^{{X}}\big{)}\circ-^{{X\times
Y}}\big{]}(x,y):=(\big{(}f\circ\pi^{{X}}\big{)}\big{(}-^{{X}}x,-^{{Y}}y\big{)}:=f(-^{{X}}x):=f_{-}(x):=\big{(}f_{-}\circ\pi^{{X}}\big{)}(x,y)$

i.e., $(\big{(}f\circ\pi^{{X}}\big{)}\circ-^{{X\times
Y}}=f_{-}\circ\pi^{{X}}\in F\times G$, since $f_{-}\in F$. Similarly,
$\big{(}g\circ\pi^{{Y}}\big{)}\circ-^{{X\times Y}}\in F\times G$. ∎

Since the projections $\pi^{{X}},\pi^{{Y}}$ are homomorphisms, they are Bishop
homomorphisms. By the universal property of the product Bishop topology,
$\boldsymbol{\mathcal{F}\times\mathcal{G}}$ is the product in BTopGrp.

##  5 Closed subsets in Bishop topological groups

######  Proposition 5.1.

Let $C\subseteq X$ and $x_{0}\in X$.
(i) If $C$ is closed, then $-C:=\\{-c\mid c\in C\\}$ is closed.
(ii) $\overline{-C}=-\overline{C}$.
(iii) If $C$ is closed, then $x_{0}+C:=\\{x_{0}+c\mid c\in C\\}$ is closed.
(iv) $\overline{x_{0}+C}=x_{0}+\overline{C}$.

###### Proof.

(i) We suppose that $u\in\overline{-C}$ i.e., if $f(u)>0$, there is $w\in-C$
such that $f(w)>0$, for every $f\in F$, and we show that $u\in-C$ i.e., $-u\in
C$. Since $C$ is closed, it suffices to show that $-u\in\overline{C}$. Let
$f\in F$ such that $f(-u)>0:\Leftrightarrow f_{-}(u)>0$. By our hypothesis on
$u$ there is $w\in-C$ such that $f_{-}(w):=f(-w)>0$, and $-w\in C$.
(ii) Since $C\subseteq\overline{C}$, we get $-C\subseteq-\overline{C}$. Since
$\overline{C}$ is closed, by (i) $-\overline{C}$ is also closed, hence
$\overline{-C}\subseteq\overline{-\overline{C}}=-\overline{C}$. To show the
converse inclusion $-\overline{C}\subseteq\overline{-C}$, let
$x\in-\overline{C}$, hence $-x\in\overline{C}$ i.e., if $f(-x)>0$, there is
$u\in C$ with $f(c)>0$, for every $f\in F$. We show that $x\in\overline{-C}$.
Let $f\in F$ with $f(x)=f(-(-x))=f_{-}(-x)>0$. By our hypothesis on $-x$,
there $u\in C$ with $f_{-}(c):=f(-u)>0$, and $-u\in-C$.
(iii) We suppose that $y\in\overline{x_{0}+C}$ i.e., if $f(y)>0$, there is
$c\in C$ such that $f(x_{0}+c)>0$, for every $f\in F$, and we show that $y\in
x_{0}+C$ by showing that $-x_{0}+y\in C$. As $C$ is closed, it suffices to
show that $-x_{0}+y\in\overline{C}$. Let $f\in F$ such that
$f(-x_{0}+y)>0\Leftrightarrow f^{1}_{-x_{0}}(y)>0$. We show that there is
$c\in C$ such that $f(c)>0$. By our hypothesis on $y$, there is $c\in C$ such
that $f^{1}_{-x_{0}}(x_{0}+c):=f(-x_{0}+x_{0}+c)=f(c)>0$.
(iv) Since $\overline{C}$ is closed, and $x_{0}+C\subseteq
x_{0}+\overline{C}$, we get
$\overline{x_{0}+C}\subseteq\overline{x_{0}+\overline{C}}=x_{0}+\overline{C}$.
For the converse inclusion, let $x:=x_{0}+y$ with $y\in\overline{C}$. We show
that $x\in\overline{x_{0}+C}$. Let $f\in F$ such that
$f(x_{0}+y)>0\Leftrightarrow f^{1}_{x_{0}}(y)>0$. We find $c\in C$ such that
$f(x_{0}+c)>0$. By our hypothesis on $y$ though, there is $c\in C$ such that
$f^{1}_{x_{0}}(c):=f(x_{0}+c)>0$. ∎

######  Corollary 5.2.

$F$ separates the points of $X$ if and only if $\\{0^{X}\\}$ is closed.

###### Proof.

If $\\{0^{X}\\}$ is closed, then by Proposition 5.1(iii)
$\\{x\\}=x+\\{0^{X}\\}$ is closed, for every $x\in X$. By Proposition 3.3 $F$
is separating. The converse follows immediately from Proposition 3.3. ∎

######  Proposition 5.3.

If $C$ is an open subgroup of $X$, then $C$ is closed in $X$

###### Proof.

Let $x\in\overline{C}$ i.e., if $f(x)>0$, there is $u\in C$ such that
$f(u)>0$, for every $h\in F$. We show that $x\in C$. Since $C$ is a subgroup
of $X$, we have that $0\in C$. Since $C$ is open in $X$, there is $g\in F$
such that $g(0)>0$ and $U(g)\subseteq C$. Since $g_{-x}^{1}\in F$ and

$g_{-x}^{1}(x):=g(-x+x)=g(0)>0,$

by our hypothesis on $x$ there is $u\in C$ such that
$g_{-x}^{1}(u):=g(-x+u)>0$. Since $U(g)\subseteq C$, we get $-x+u\in C$, and
since $C$ is a subgroup of $X$, we get $x\in C$. ∎

Classically, $C$ is closed, since its complement in $X$ is the open set
$\bigcup\\{x+C\mid x\notin C\\}$, where $x+C$ is open, for every $x\in X$, as
$C$ is open (this holds also constructively). The double use of negation in
the classical proof is replaced here by the clear algorithm of the previous
proof.

######  Lemma 5.4.

The commutator map $\textnormal{{abel}}:X\times X\to X$ is defined by
$\textnormal{{abel}}(x,y):=x+y-x-y,$ , for every $(x,y)\in X\times X$.
(i)
$\textnormal{{abel}}\in\mathrm{Mor}(\mathcal{F}\times\mathcal{F},\mathcal{F})$.
(ii) If $x,y\in X$, then
$x+y=_{X}y+x\Leftrightarrow\textnormal{{abel}}(x,y)=0^{X}$.
(iii) If $x\in X$, the mapping $\textnormal{{abel}}_{x}:X\to X$, where
$\textnormal{{abel}}_{x}(y):=\textnormal{{abel}}(x,y)$, for every $y\in X$, is
in $\mathrm{Mor}(\mathcal{F},\mathcal{F})$, and for every $f\in F$ the
composition $f\circ\textnormal{{abel}}_{x}\in F$

$X$$X$${\mathbb{R}}$.${\textnormal{{abel}}_{x}}$$f$${f\circ\textnormal{{abel}}_{x}}$

(iv) If $x,y\in X$, then
$\textnormal{{abel}}_{x}(y)=-\textnormal{{abel}}_{y}(x)$.
(v) If $x,y\in X$, then
$\textnormal{{abel}}_{x}(y)=0^{X}\Leftrightarrow\textnormal{{abel}}_{y}(x)=0^{X}$.

###### Proof.

(i) By the definition of the product Bishop topology
$\pi_{1},\pi_{2}\in\mathrm{Mor}(\mathcal{F}\times\mathcal{F},\mathcal{F})$.
Since $\textnormal{{abel}}:=\pi_{1}+\pi_{2}-\pi_{1}-\pi_{2}$, by Proposition
4.7 we get
$\textnormal{{abel}}\in\mathrm{Mor}(\mathcal{F}\times\mathcal{F},\mathcal{F})$.
(ii) and (iii) The proof for (ii) is immediate. By (i) and Proposition
2.5(iii) $\textnormal{{abel}}_{x}\in\mathrm{Mor}(\mathcal{F},\mathcal{F})$,
hence by the definition of a Bishop morphism $f\circ\textnormal{{abel}}_{x}\in
F$, for every $f\in F$.
(iv) is trivial and (v) follows immediately from (iv). ∎

######  Lemma 5.5.

Let $x\in X$ and $H\subseteq X$. The maps $\textnormal{{normal}}_{x}:X\to X$
and $\textnormal{{Normal}}_{x}:X\to X$ are defined, for every $x\in X$,
respectively, by $\textnormal{{normal}}_{x}(y):=x+y-x$ and
$\textnormal{{Normal}}_{x}(y):=y+x-y$. Let
$\textnormal{{normal}}_{x}^{{H}},\textnormal{{Normal}}_{x}^{{H}}:H\to X$ be
the restrictions of $\textnormal{{normal}}_{x}$ and
$\textnormal{{Normal}}_{X}$ to $H$, respectively.
(i) If $x,y\in X$, then
$\textnormal{{normal}}_{x}(y)=\textnormal{{Normal}}_{y}(x)$.
(ii) $\textnormal{{normal}}_{x}\in\mathrm{Mor}(\mathcal{F},\mathcal{F})$ and
$\textnormal{{Normal}}_{x}\in\mathrm{Mor}(\mathcal{F},\mathcal{F})$.
(iii) If $H\leq X$, then $H$ is normal if and only if
$\textnormal{{normal}}_{x}^{{H}}:H\to H$, for every $x\in X$.
(iv) If $f\in F$, the compositions $f\circ\textnormal{{normal}}_{x}\in F$ and
$f\circ\textnormal{{Normal}}_{x}\in F$.

$X$$X$${\mathbb{R}}$.$X$${\mathbb{R}}$${\textnormal{{normal}}_{x}}$$\ \
{f}$${f}$${f\circ\textnormal{{normal}}_{x}}$$\ \
{\textnormal{{Normal}}_{x}}$${f\circ\textnormal{{Normal}}_{x}}$

(v) If $H$ is normal, then
$\textnormal{{normal}}_{x}^{{H}}\in\mathrm{Mor}\big{(}\mathcal{F}_{|H},\mathcal{F}_{|H}\big{)}$.
(vi) If $\textnormal{{Normal}}_{x}^{{H}}:H\to H$, then
$\textnormal{{Normal}}_{x}^{{H}}\in\mathrm{Mor}\big{(}\mathcal{F}_{|H},\mathcal{F}_{|H}\big{)}$.

###### Proof.

(i) The proof is immediate. For the proof of (ii), the function $c_{x}:X\to
X$, defined by $c_{x}(y):=x$, for every $y\in X$, is in
$\mathrm{Mor}(\mathcal{F},\mathcal{F})$; if $f\in F$, then $(f\circ
c_{x})(y):=f(x)$, for every $y\in X$, hence $f\circ
c_{x}=\overline{f(x)}^{{X}}\in F$. The identity map $\mathrm{id}_{X}$ on $X$
is also in $\mathrm{Mor}(\mathcal{F},\mathcal{F})$. Since
$\textnormal{{normal}}_{x}:=c_{x}+\mathrm{id}_{X}-c_{x}$, by Proposition 4.7
$\textnormal{{normal}}_{x}\in\mathrm{Mor}(\mathcal{F},\mathcal{F})$. Since
$\textnormal{{Normal}}_{x}:=\mathrm{id}_{X}+c_{x}-\mathrm{id}_{X}$, we get
$\textnormal{{Normal}}_{x}\in\mathrm{Mor}(\mathcal{F},\mathcal{F})$. (iii) and
(iv) are immediate to show. For the proof of (v), by the $\bigvee$-lifting of
morphisms we have that
$\textnormal{{normal}}_{x}^{{H}}\in\mathrm{Mor}\big{(}\mathcal{F}_{|H},\mathcal{F}_{|H}\big{)}$
if and only if $\forall_{f\in
F}\big{(}f_{|H}\circ\textnormal{{normal}}_{x}^{{H}}\in F_{|H}\big{)}.$ If
$f\in F$ and $v\in H$, then
$\big{(}f_{|H}\circ\textnormal{{normal}}_{x}^{{H}}\big{)}(v):=f_{|H}(x+v-x):=f(x+v-x):=\big{(}f\circ\textnormal{{normal}}_{x}\big{)}(v):=\big{(}f\circ\textnormal{{normal}}_{x}\big{)}_{|H}(v)$
i.e.,
$f_{|H}\circ\textnormal{{normal}}_{x}^{{H}}=\big{(}f\circ\textnormal{{normal}}_{x}\big{)}_{|H}\in
F_{|H}$, since $f\circ\textnormal{{normal}}_{x}\in F$. For the proof of (vi),
we proceed as in the proof of (v). ∎

######  Theorem 5.6.

Let $H$ be a subgroup of $X$.
(i) The closure $\overline{H}$ of $H$ is also a subgroup of $X$.
(ii) If $F$ is a separating Bishop topology and $H$ is abelian, then
$\overline{H}$ is abelian.
(iii) If $H$ is normal, then $\overline{H}$ is normal.

###### Proof.

(i) Since $H\subseteq\overline{H}$ and $0\in H$, we get $0\in\overline{H}$.
Let $x,y\in\overline{H}$, where by definition

$x\in\overline{H}:\Leftrightarrow\forall_{f\in
F}\big{(}f(x)>0\Rightarrow\exists_{v\in H}(f(v)>0)\big{)},$
$y\in\overline{H}:\Leftrightarrow\forall_{f\in
F}\big{(}f(y)>0\Rightarrow\exists_{v\in H}(f(v)>0)\big{)}.$

We show that $x+y\in\overline{H}$ i.e., $\forall_{f\in
F}\big{(}f(x+y)>0\Rightarrow\exists_{v\in H}(f(v)>0)\big{)}$. Let $f\in F$
such that $f(x+y)>0$. By Proposition 4.4(iii) the map
$f_{y}^{2}:X\to{\mathbb{R}}\in F$, where $f_{y}^{2}(u):=f(u+y)$, for every
$u\in X$. By hypothesis, $f_{y}^{2}(x)>0$. Since $x\in\overline{H}$, there is
$z\in H$ such that

$f_{y}^{2}(z)>0:\Leftrightarrow f(z+y)>0:\Leftrightarrow f_{z}^{1}(y)>0,$

where by Proposition 4.4(iii) the map $f_{z}^{1}:X\to{\mathbb{R}}\in F$, where
$f_{z}^{1}(u):=f(z+u)$, for every $u\in X$, is in $F$. Since
$y\in\overline{H}$, there is $w\in H$ such that
$f_{z}^{1}(w)>0:\Leftrightarrow f(z+w)>0$. Since $H\leq X$, we get $z+w\in H$,
which is what we need to show. Next we show that $-x\in\overline{H}$ i.e.,

$\forall_{f\in F}\big{(}f(-x)>0\Rightarrow\exists_{v\in H}(f(v)>0)\big{)}.$

Let $f\in F$ such that $f(-x)>0\Leftrightarrow f_{-}(x)>0$. Since $f_{-}\in F$
and $x\in\overline{H}$, there is $v\in H$ such that $f_{-}(v):=f(-v)>0$. Since
$H\leq X$, we get $-v\in H$, and our proof is completed.
(ii) Case I: $x\in H$ and $y\in\overline{H}$.
We show that $\textnormal{{abel}}_{x}(y)=_{{X}}0^{{X}}$. Suppose that
$\textnormal{{abel}}_{x}(y)\neq_{{F}}0^{{X}}$. By Proposition 5.2.5 in [28]
there is $f\in F$ such that $f\big{(}\textnormal{{abel}}_{x}(y)\big{)}=1$ and
$f\big{(}0^{{X}}\big{)}=0$. Since $y\in\overline{H}$, and
$(f\circ\textnormal{{abel}}_{x})(y)=1>0$, and
$f\circ\textnormal{{abel}}_{x}\in F$, there is $v\in H$ such that
$(f\circ\textnormal{{abel}}_{x})(v)>0$. Since $x,v\in H$ and $H$ is abelian,
we have that $\textnormal{{abel}}_{x}(v)=0^{{X}}$, hence
$0=f\big{(}0^{{X}}\big{)}=(f\circ\textnormal{{abel}}_{x})(v)>0$, which is a
contradiction. Since $F$ is separating, the canonical apartness relation
$\neq_{F}$ of $F$ is tight (see Proposition 5.1.3 in [28]), hence the negation
of $\textnormal{{abel}}_{x}(y)\neq_{{F}}0^{{X}}$ implies that
$\textnormal{{abel}}_{x}(y)=_{{X}}0^{{X}}$.
Case II: $x\in\overline{H}$ and $y\in\overline{H}$.
We show that $\textnormal{{abel}}_{x}(y)=_{{X}}0^{{X}}$. Suppose that
$\textnormal{{abel}}_{x}(y)\neq_{{F}}0^{{X}}$. As in the previous case, there
is $f\in F$ such that $f\big{(}\textnormal{{abel}}_{x}(y)\big{)}=1$ and
$f\big{(}0^{{X}}\big{)}=0$. Since $y\in\overline{H}$, and
$(f\circ\textnormal{{abel}}_{x})(y)=1>0$, there is $v\in H$ such that
$(f\circ\textnormal{{abel}}_{x})(v)>0$. By case I we have that
$\textnormal{{abel}}_{v}(x)=0^{{X}}$, hence by Lemma 5.4(v) we get
$\textnormal{{abel}}_{x}(v)=0^{{X}}$, hence
$0=f\big{(}0^{{X}}\big{)}=(f\circ\textnormal{{abel}}_{x})(v)>0$, which is a
contradiction. Since $F$ is separating, we conclude, similarly to Case I, that
$\textnormal{{abel}}_{x}(y)=_{{X}}0^{{X}}$.
(iii) By Lemma 5.5(ii) it suffices to show that
$\textnormal{{normal}}_{x}^{{\overline{H}}}:\overline{H}\to\overline{H}$, for
every $x\in X$. If $x\in X$ and $y\in\overline{H}$, we show that

$\textnormal{{normal}}_{x}^{{\overline{H}}}(y):=x+y-x\in\overline{H}.$

Let $f\in F$ such that
$f(x+y-x)>0\Leftrightarrow(f\circ\textnormal{{normal}}_{x})(y)>0$. We need to
find $u\in H$ such that $f(u)>0$. Since $y\in\overline{H}$ and
$f\circ\textnormal{{normal}}_{x}\in F$, there is $v\in H$ with

$(f\circ\textnormal{{normal}}_{x})(v):=f(x+v-x)>0.$

Since $H$ is normal and $v\in H$, we have that $u:=x+v-x\in H$ and $f(u)>0$. ∎

As we explain in [28], section 5.8, by the Stone-Čech theorem for Bishop
spaces we have that the separating hypothesis on $F$ in case (ii) of the
previous proposition is not a serious restriction on $F$. Note that
classically, if $X$ is a Hausdorff topological group, then if $H$ is an
abelian subgroup, then $\overline{H}$ is abelian. The $F$-version of a
Hausdorff topology is the following (see [28], section 5.2): if $\neq$ is a
given apartness relation on $X$, then $F$ is $\neq$-Hausdorff, if
$\neq\subseteq\neq_{F}$. In Proposition 5.2.3. of [28] we show that this is
equivalent to the positive $\neq$-version of the induced neighborhood
structure being Hausdorff. If $F$ is $\neq$-Hausdorff, $n$-many pairwise
$\neq$-apart points of $X$ are mapped to given $n$-many real numbers. This is
essential to the proof we gave above. So, we capture computationally the
requirement of a Hausdorff topology for $\overline{H}$ being abelian. By
Proposition 3.3 the tightness of $\neq_{F}$ in a Bishop topological group
implies that the induced topology is Hausdorff in the classical sense
(classically, a topological group is Hausdorff if and only if there is a
closed singleton). In the next proposition the subset $H$ of $X$ is
extensional i.e., $H$ is closed under the given equality $=_{X}$ on $X$, so
that the defining property of $\textnormal{{Normal}}_{X}(H)$ in the use of the
separation scheme is also extensional.

######  Theorem 5.7.

Let $H$ be an extensional subset of $X$. The normalizer
$\textnormal{{Normal}}_{X}(H)$ and the center $\textnormal{{Center}}_{X}(H)$
of $H$ in $X$, are defined by

$\textnormal{{Normal}}_{X}(H):=\big{\\{}x\in
X\mid\textnormal{{Normal}}_{x}^{{H}}:H\to H\big{\\}},$
$\textnormal{{Center}}_{X}(H):=\big{\\{}x\in X\mid\forall_{v\in
H}\big{(}\textnormal{{abel}}_{x}(v)=0^{{X}}\big{)}\big{\\}}.$

(i) If $H$ is closed, then $\textnormal{{Normal}}_{X}(H)$ is closed.
(ii) If $F$ is separating, then $\textnormal{{Center}}_{X}(H)$ is closed.

###### Proof.

(i) We suppose that $H$ is closed i.e.,

$(\textnormal{{Hyp}}_{1})\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\ \ \forall_{x\in X}\bigg{(}\forall_{f\in
F}\big{(}f(x)>0\Rightarrow\exists_{v\in
H}\big{(}f(v)>0\big{)}\big{)}\Rightarrow x\in H\bigg{)},\ \ \ \ \ \ \ \ \ \ \
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $

and we show that $\textnormal{{Normal}}_{X}(H)$ is closed i.e.,

$(\textnormal{{Goal}}_{1})\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \forall_{x\in
X}\bigg{(}\forall_{f\in
F}\big{(}f(x)>0\Rightarrow\exists_{u\in\textnormal{{Normal}}_{X}(H)}\big{(}f(u)>0\big{)}\big{)}\Rightarrow
x\in\textnormal{{Normal}}_{X}(H)\bigg{)}.\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
$

For that we fix some $x\in X$ and we suppose that

$(\textnormal{{Hyp}}_{2})\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\ \ \ \ \ \ \forall_{f\in
F}\big{(}f(x)>0\Rightarrow\exists_{u\in\textnormal{{Normal}}_{X}(H)}\big{(}f(u)>0\big{)}\big{)},\
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\ \ \ \ \ $

and we show that $(\textnormal{{Goal}}_{2})\ \
x\in\textnormal{{Normal}}_{X}(H):\Leftrightarrow\textnormal{{Normal}}_{x}^{{H}}:H\to
H$. Let $v\in H$ be fixed, and we show $(\textnormal{{Goal}}_{3})\ \
\textnormal{{Normal}}_{x}^{{H}}(v):=v+x-v\in H.$ By $\textnormal{{Hyp}}_{1}$
it suffices to show the following

$(\textnormal{{Goal}}_{4})\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\ \ \ \ \ \ \ \forall_{f\in
F}\bigg{(}f\big{(}\textnormal{{Normal}}_{x}^{{H}}(v)\big{)}>0\Rightarrow\exists_{w\in
H}\big{(}f(w)>0\big{)}\bigg{)}.\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $

If we fix $f\in F$, we suppose that

$(\textnormal{{Hyp}}_{3})\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
f\big{(}\textnormal{{Normal}}_{x}^{{H}}(v)\big{)}>0\Leftrightarrow
f\big{(}\textnormal{{normal}}_{v}(x)\big{)}>0\Leftrightarrow(f\circ\textnormal{{normal}}_{v}))(x)>0,\
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $

and we show $(\textnormal{{Goal}}_{5})\ \ \exists_{w\in
H}\big{(}f(w)>0\big{)}$. Since $f\circ\textnormal{{normal}}_{v}\in F$, by
$(\textnormal{{Hyp}}_{2})$ there is $u\in\textnormal{{Normal}}_{X}(H)$ with
$(f\circ\textnormal{{normal}}_{v})(u):=f(v+u-v)>0$. Since
$u\in\textnormal{{Normal}}_{X}(H)$, $\textnormal{{Normal}}_{u}^{{H}}:H\to H$,
and since $v\in H$, we get $\textnormal{{Normal}}_{u}^{{H}}(v):=v+u-v\in H$.
Hence, $w:=v+u-v\in H$ and $f(w)>0$.
(ii) We fix $x\in X$, we suppose that

$(\textnormal{{Hyp}}_{1}^{*})\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\ \ \ \ \ \ \ \ \forall_{f\in
F}\big{(}f(x)>0\Rightarrow\exists_{u\in\textnormal{{Center}}_{X}(H)}\big{(}f(u)>0\big{)}\big{)},\
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\ \ \ \ \ $

and we show $(\textnormal{{Goal}}_{1}^{*})\ \
x\in\textnormal{{Center}}_{X}(H):\Leftrightarrow\forall_{v\in
H}\big{(}\textnormal{{abel}}_{x}(v)=0^{{X}}\big{)}$. Let $v\in H$ be fixed.
Since $F$ is a separating Bishop topology, it suffices to prove
$\neg\big{(}\textnormal{{abel}}_{x}(v)\neq_{F}0^{{X}}\big{)}$. If we suppose
that $\textnormal{{abel}}_{x}(v)\neq_{F}0^{{X}}$, there is $f\in F$ such that

$f\big{(}\textnormal{{abel}}_{x}(v)\big{)}=1>0\ \ \ \&\ \ \
f\big{(}0^{{X}}\big{)}=0.$

By Lemma 5.4(iv) we get

$1=f\big{(}\textnormal{{abel}}_{x}(v)\big{)}=f\big{(}-\textnormal{{abel}}_{v}(x)\big{)}:=f_{-}\big{(}\textnormal{{abel}}_{v}(x)\big{)}\
\ \ \&\ \ \ 0=f\big{(}0^{{X}}\big{)}=f_{-}\big{(}0^{{X}}\big{)}.$

Since $f_{\in}F$, we have that $f_{-}\circ\textnormal{{abel}}_{v}\in F$ and
$(f_{-}\circ\textnormal{{abel}}_{v})(x)>0$. By $(\textnormal{{Hyp}}_{1}^{*})$
there is $u\in\textnormal{{Center}}_{X}(H)$ such that
$(f_{-}\circ\textnormal{{abel}}_{v})(u)>0$. Since
$u\in\textnormal{{Center}}_{X}(H)$, we get $\forall_{w\in
H}\big{(}\textnormal{{abel}}_{u}(w)=0^{{X}}\big{)}$. Moreover,
$(f_{-}\circ\textnormal{{abel}}_{v})(u):=f_{-}(v+u-v-u)>0$. Since $v\in H$, we
get

$v+u-v-u:=\textnormal{{abel}}_{v}(u)=-\textnormal{{abel}}_{u}(v)=-0^{{X}}=0^{{X}},$

hence $f_{-}\big{(}0^{{X}}\big{)}>0$, which contradicts the previously
established equality $f_{-}\big{(}0^{{X}}\big{)}=0^{{X}}$. ∎

######  Proposition 5.8.

If $G$ is a separating Bishop topology on $Y$ and
$h\in\textnormal{{Mor}}(\boldsymbol{\mathcal{F}},\boldsymbol{\mathcal{G}})$,
the kernel $\textnormal{{Ker}}(h):=\big{\\{}x\in X\mid
h(x)=_{Y}0^{{Y}}\big{\\}}$ of $h$ is a closed set in $\mathcal{F}$.

###### Proof.

Let $x\in X$ such that $\forall_{f\in
F}\big{(}f(x)>0\Rightarrow\exists_{v\in\textnormal{{Ker}}(h)}\big{(}f(v)>0\big{)}\big{)}$.
Since $\neq_{G}$ is tight, it suffices to show that
$\neg\big{(}h(x)\neq_{G}0^{{Y}}\big{)}$. If $h(x)\neq_{G}0^{{Y}}$, there is
$g\in G$ such that $g(h(x))=1>0$ and $g\big{(}0^{{Y}}\big{)}=0$. Since
$h\in\mathrm{Mor}(\mathcal{F},\mathcal{G})$, we have that $g\circ h\in F$. As
$(g\circ h)(x)>0$, there is $v\in\textnormal{{Ker}}(h)$ such that
$0=g\big{(}0^{{Y}}\big{)}=g(h(v)):=(g\circ h)(v)>0$, which is a contradiction.
∎

######  Theorem 5.9 (Characterisation of a closed (open) subgroup).

Let $C$ be a subgroup of $X$.
(i) $C$ is closed if and only if there is an open set $O$ in $X$ such that
$O\cap C$ is inhabited and closed in $O$.
(ii) $C$ is open if and only if there is an inhabited, open set $O$ in $X$
such that $O\subseteq C$.

###### Proof.

(i) Let $O$ be open in $X$ such that $O\cap C$ is inhabited and closed in $O$.
We show that $C$ is closed. Suppose that $x\in\overline{C}$ i.e., i.e., if
$f(x)>0$, there is $u\in C$ such that $f(u)>0$, for every $h\in F$. We prove
that $x\in C$. Let $c_{0}\in O\cap C$. Since $O$ is open, there is $g\in F$
such that $g(c_{0})>0$ and $U(g)\subseteq O$. Since $g^{1}_{-x+c_{0}}\in F$
and

$g^{1}_{-x+c_{0}}(x):=g(x-x+c_{0})=g(c_{0})>0,$

by our hypothesis on $x$ there is $c\in C$ such that

$g^{1}_{-x+c_{0}}(c):=g(c-x+c_{0})>0.$

As $U(g)\subseteq O$, we get $c-x+c_{0}\in O$. The hypothesis “$O\cap C$ is
closed in $O$” means

$\forall_{z\in O}\big{(}z\in\overline{O\cap C}\Rightarrow z\in O\cap
C\big{)}.$

Let $z_{0}:=c-x+c_{0}\in O$. We show that $z_{0}\in\overline{O\cap C}$, hence
$z_{0}\in O\cap C$. Since $C$ is a subspace, and since then $z_{0}\in C$, we
get the required membership $x\in C$. To show that $z_{0}\in\overline{O\cap
C}$, let $f\in F$ such that $f(z_{0})>0$. We find $w\in O\cap C$ such that
$f(w)>0$. Since $f(z_{0})>0$ and $g(z_{0})>0$, we have that $(f\wedge
g)(z_{0})>0$ (see [8], p. 57). By Theorem 5.6(i) $\overline{C}$ is a subgroup
of $X$. Since $C\subseteq\overline{C}$, and $c,c_{0},-x\in\overline{C}$, we
get $z_{0}\in\overline{C}$. Since $f\wedge g\in F$ and $(f\wedge g)(z_{0})>0$,
there is $w\in C$ such that

$(f\wedge g)(w)>0.$

Since $g(w)\geq(f\wedge g)(w)>0$, we get $w\in O$, hence $w\in O\cap C$. Since
$f(w)\geq(f\wedge g)(w)>0$, we conclude that $f(w)>0$, as required. For the
converse, if $C$ is closed, then $X$ is open, $C=C\cap X$ is inhabited by $0$
and it is trivially closed in $X$.
(ii) Let $O$ be open in $X$ such that $O\subseteq C$, and let $c_{0}\in O$.
Suppose that $g\in F$ with $g(c_{0})>0$ and $U(g)\subseteq O$. Since also
$U(g)\subseteq C$, we get $c_{0}\in C$. Let $c\in C$. The function
$g^{1}_{-c+c_{0}}\in F$ and $g^{1}_{-c+c_{0}}(c)=g(c_{0})>0$. We show that
$U(g^{1}_{-c+c_{0}})\subseteq C$, hence, since $c$ is an arbitrary element of
$C$, we conclude that $C$ is open. Let $u\in X$ such that
$g^{1}_{-c+c_{0}}(u):=g(u-c+c_{0})>0$. As $U(g)\subseteq O\subseteq C$, we get
$u-c+c_{0}\in C$. As $c,c_{0}\in C$ and $C$ is a subgroup of $X$, we have that
$u\in C$. For the converse, if $C$ is open, then $C$ is an inhabited open set
included in $C$. ∎

The classical proof of Theorem 5.9(i) is based on multiple use of negation
(see [21]). As usual in constructive mathematics, we replaced the “non-empty
intersection” of $O$ and $C$ in Theorem 5.9(i) with $O\between C$, and the
“non-emptyness” of $O$ in Theorem 5.9(ii) with the stronger inhabitedness of
$O$. Although, in general, it is not possible to show that the $F$-complement
$X\setminus_{F}C$ of a closed set in a Bishop space $X$ is equal to
$X\setminus C$, there is a number of cases in the theory of Bishop topological
groups where this is possible.

######  Corollary 5.10.

If $C$ is closed in $X$, such that $X\setminus C$ is a subgroup of $X$ and
$X\setminus_{F}C$ is inhabited, then $X\setminus C=X\setminus_{F}C$ and
$X\setminus C$ is clopen.

###### Proof.

By Theorem 3.2 we have that $X\setminus_{F}C$ is open in $X$ and
$X\setminus_{F}C\subseteq X\setminus C$. Since $X\setminus_{F}C$ is inhabited
and $X\setminus C$ is a subgroup of $X$, by Theorem 5.9(ii) we have that
$X\setminus C$ is open. As $X\setminus C\subseteq X\setminus C$, by Theorem
3.2 we get $X\setminus C\subseteq X\setminus_{F}C$, hence $X\setminus
C=X\setminus_{F}C$. As $X\setminus C$ is an open subgroup, by Proposition 5.3
we have that $X\setminus C$ is also closed. ∎

Notice that classically a subgroup $C$ of a topological group is either clopen
or has empty interior. By replacing the hypothesis of “non-empty interior of
$C$” with the positive “existence of an inhabited open subset of $C$”,
constructively we have the following corollary.

######  Corollary 5.11.

Let $C$ be a subgroup of $X$. If $O$ is an inhabited open set in $X$ such that
$O\subseteq C$, then $C$ is clopen.

###### Proof.

By Theorem 5.9(ii) $C$ is open, and by Proposition 5.3 $C$ is also closed. ∎

Here we have presented some very first, fundamental results in the theory of
Bishop topological groups. Clearly, we can work similarly for other algebraic
structures, like rings and modules, equipped with a compatible Bishop
topology. There is a plethora of open questions related to Bishop topological
groups. The complete regularity of a Bishop topological group, the study of
“compact” subsets of Bishop topological groups, the uniform continuity of the
elements of $F$ when $X$ is a compact Bishop topological group with $F$, and
the interpretation of local compactness in the theory of Bishop topological
groups, are some of the numerous topics to which our future work could
hopefully be directed.

Acknowledgements: The content of this paper was part of my talk in “Conference
Algebra and Algorithms” that took place in Djerba, Tunisia, in February 2020.
I would like to thank the organisers, Peter Schuster and Ihsen Yengui, for
inviting me. This research was supported by LMUexcellent, funded by the
Federal Ministry of Education and Research (BMBF) and the Free State of
Bavaria under the Excellence Strategy of the Federal Government and the
Länder.

## References

  * [1] P. Aczel, M. Rathjen: Constructive Set Theory, book draft, 2010.
  * [2] A. Arhangel’skii, M. Tkachenko: Topological Groups and Related Structures, Atlantis Press$/$World Scientific, 2008.
  * [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, F. Richman: Varieties of Constructive Mathematics, Cambridge University Press, 1987.
  * [7] D. S. Bridges and L. S. Vîţă: Techniques of Constructive Analysis, in: Universitext, Springer, New York, 2006.
  * [8] D. S. Bridges, L. S. Vîţă: Apartness and Uniformity: A Constructive Development, in: CiE series Theory and Applications of Computability, Springer Verlag, Berlin Heidelberg, 2011.
  * [9] D. Bridges, E. Palmgren: Constructive Mathematics; Approaches to Constructive Topology, Stanford Encyclopedia of Philosophy, 2018.
  * [10] D. S. Bridges: Constructive complements of unions of two closed sets, Math. Log. Quart. 50, No. 3, 2004, 293–294.
  * [11] D. S. Bridges: Reflections on function spaces, Annals of Pure and Applied Logic 163, 2012, 101–110.
  * [12] T. Coquand, P. Dybjer, E. Palmgren, A. Setzer: Type-theoretic Foundations of Constructive Mathematics, book-draft, 2005.
  * [13] L. Crosilla and P. Schuster (Eds.) From Sets and Types to Topology and Analysis, Towards Practical Foundations for Constructive Mathematics, Clarendon Press, Oxford, 2005.
  * [14] M. H. Escardó, C. Xu: A constructive manifestation of the Kleene-Kreisel continuous functionals, Ann. Pure Appl. Logic, 167(9), 2016, 770-793.
  * [15] J. Geins: Bridges between the theory of Bishop spaces and the theory of $C$-spaces, Master Thesis, Mathematics Institute LMU, 2018.
  * [16] P. J. Higgins: Introduction to Topological Groups, Cambridge University Press, 1974.
  * [17] H. Ishihara, R. Mines, P. Schuster, L. S. Vîţă: Quasi-apartness and neighborhood spaces, Annals of Pure and Applied Logic 141, 2006, 296–306.
  * [18] H. Ishihara: Two subcategories of apartness spaces, Annals of Pure and Applied Logic 163, 2013, 132–139.
  * [19] H. Ishihara: Relating Bishop’s function spaces to neighborhood spaces, Annals of Pure and Applied Logic 164, 2013, 482–490.
  * [20] H. Ishihara and E. Palmgren: Quotient topologies in constructive set theory and type theory, Annals of Pure and Applied Logic 141, 2006, 257–265.
  * [21] L. Kramer: Locally compact groups, Lecture Notes, 2017.
  * [22] P. Martin-Löf: Notes on Constructive Mathematics, Almqvist and Wiksell, 1968.
  * [23] P. Martin-Löf: Intuitionistic type theory: Notes by Giovanni Sambin on a series of lectures given in Padua, June 1980, Napoli: Bibliopolis, 1984.
  * [24] R. Mines, F. Richman, W. Ruitenburg: A Course in Constructive Algebra, Springer Science$+$Business Media New York, 1988.
  * [25] J. Myhill: Constructive Set Theory, J. Symbolic Logic 40, 1975, 347–382.
  * [26] R. S. Lubarsky, M. Rathjen: On the regular extension axiom and its variants, Mathematical Logic Quarterly 49 (5), 2003, 511–518.
  * [27] I. Petrakis: Completely Regular Bishop Spaces, in A. Beckmann et. al. (Eds.) Evolving Computability, CiE 2015, LNCS 9136, 2015, 302–312.
  * [28] I. Petrakis: Constructive Topology of Bishop Spaces, PhD Thesis, LMU Munich, 2015.
  * [29] 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.
  * [30] 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.
  * [31] I. Petrakis: Constructive uniformities of pseudometrics and Bishop topologies, Journal of Logic and Analysis, 11:FT2, 2019, 1–44.
  * [32] I. Petrakis: Borel and Baire sets in Bishop Spaces, in F. Manea et. al. (Eds): CiE 2019, LNCS 11558, 2019, 240–252.
  * [33] I. Petrakis: Direct spectra of Bishop spaces and their limits, in Logical Methods in Computer Science, to appear, 2021.
  * [34] I. Petrakis: Embeddings of Bishop spaces, Journal of Logic and Computation, exaa015, 2020, https://doi.org/10.1093/logcom/exaa015.
  * [35] 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.
  * [36] I. Petrakis: Families of Sets in Bishop Set Theory, Habilitationsschrift, LMU, Munich, 2020\.
  * [37] F. Richman: Constructive mathematics without choice, in [40], pp.199–205.
  * [38] G. Sambin: Intuitionistic formal spaces - a first communication, in D. Skordev (ed.) Mathematical Logic and its Applications, Plenum Press, 1987, 187-204.
  * [39] G. Sambin: The Basic Picture: Structures for Constructive Topology, Oxford University Press, in press.
  * [40] P. Schuster, U. Berger, H. Osswald (Eds.): Reuniting the Antipodes Constructive and Nonstandard Views of the Continuum, Proc. 1999 Venice Symposium, Dordrecht: Kluwer, 2001.
  * [41] P. Schuster: Countable Choice as a Questionable Uniformity Principle, Philosophia Mathematica (3) Vol. 12, pp. 106–134, 2004.
  * [42] S. Warner: Topological Rings, North-Holland Mathematics Studies 178, Elsevier Science Publishers B.V., 1993.
  * [43] C. Xu: A continuous computational interpretation of type theories, PhD Thesis, University of Birmingham, 2015.


The problem of social cost.
Journal of Law and Economics, 3:0 1–44, 1960.

[Courty and Li, 2000]
P. Courty and H. Li.
Sequential screening.
Review of Economic Studies, 670 (4):0
697–717, 2000.

[Eső and Szentes, 2007]
P. Eső and B. Szentes.
Optimal information disclosure in auctions and the handicap auction.
Review of Economic Studies, 740 (3):0
705–731, 2007.

[Eső and Szentes, 2017]
P. Eső and B. Szentes.
Dynamic contracting: an irrelevance theorem.
Theoretical Economics, 12:0 109–139, 2017.

[Gorton and Winton, 2003]
G. Gorton and A. Winton.
Financial intermediation.
In G. M. Constantinides, M. Harris, and R. M. Stulz, editors,
Handbook of the Economics of Finance Vol. 1, chapter 8, pages
431–552. Elsevier, 2003.

[Hagerty and Rogerson, 1987]
K. M. Hagerty and W. P. Rogerson.
Robust trading mechanisms.
Journal of Economic Theory, 420 (1):0 94–107,

[Holmström and Myerson, 1983]
B. Holmström and R. B. Myerson.
Efficient and durable decision rules with incomplete information.
Econometrica, 510 (6):0 1799–1819, 1983.

[Kos and Manea, 2009]
N. Kos and M. Manea.
Efficient trade mechanism with discrete values.
Bocconi University and Harvard University, 2009.

[Kos and Messner, 2013]
N. Kos and M. Messner.
Extremal incentive compatible transfers.
Journal of Economic Theory, 1480 (1):0
134–164, 2013.

[Krasikov and Lamba, 2021]
I. Krasikov and R. Lamba.
A theory of dynamic contracting with financial constraints.
Journal of Economic Theory, 1930 (105196), 2021.

[Krishna and Perry, 2000]
V. Krishna and M. Perry.
Efficient mechanism design.
Pennsylvania State University and The Hebrew University of Jerusalem,

[Lamba, 2014]
R. Lamba.
Essays in dynamic mechanism design.
Ph.D. dissertation, Princeton University, 2014.

[Makowski and Mezzetti, 1994]
L. Makowski and C. Mezzetti.
Bayesian and weakly robust first best mechanisms: characterizations.
Journal of Economic Theory, 640 (2):0
500–519, 1994.

[Matsuo, 1989]
T. Matsuo.
On incentive compatible, individually rational, and ex post efficient
mechanisms for bilateral trading.
Journal of Economic Theory, 490 (1):0
189–194, 1989.

[Miller, 2012]
D. Miller.
Robust collusion with private information.
The Review of Economic Studies, 790 (2):0
778–811, 2012.

[Myerson, 1985]
R. B. Myerson.
Analysis of two bargaining problems with incomplete information.
In A. Roth, editor, Game-theoretic models of bargaining,
chapter 7, pages 115–147. Cambridge University Press, 1985.

[Myerson, 1986]
R. B. Myerson.
Multistage games with communication.
Econometrica, 540 (2):0 323–358, 1986.

[Myerson and Satterthwaite, 1983]
R. B. Myerson and M. A. Satterthwaite.
Efficient mechanisms for bilateral trading.
Journal of Economic Theory, 290 (2):0
265–281, 1983.

[Pavan, 2016]
A. Pavan.
Dynamic mechanism design: Robustness and endogenous types.
In 2015 World Congress of the Econometric Society, 2016.

[Pavan et al., 2014]
A. Pavan, I. Segal, and J. Toikka.
Dynamic mechanism design: A Myersonian approach.
Econometrica, 820 (2):0 601–653, 2014.

[Skrzypacz and Toikka, 2015]
A. Skrzypacz and J. Toikka.
Mechanisms for repeated trade.
American Economic Journal: Microeconomics, 70
(4):0 252–293, 2015.

[Stole, 2001]
L. Stole.
Lectures on the theory of contracts and organizations.
University of Chicago, 2001.

[Vohra, 2012]
R. V. Vohra.
Dynamic mechanism design.
Surveys in Operations Research and Management Science,
170 (1):0 60–68, 2012.

[Williams, 1999]
S. R. Williams.
A characterization of efficient, bayesian incentive compatible
Economic Theory, 140 (1):0 155–180, 1999.

[Yoon, 2015]
K. Yoon.
On budget balance of the dynamic pivot mechanism.
Games and Economic Behavior, 94:0 206–213, 2015.