\[  \ \ \ \ \ \ \ \ \ \ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \exists  \lim_{\mathsmaller{m \to + \infty}} \mu \big(\B \lambda_0 (\beta(m))\big) \  \& \ \lim_{\mathsmaller{m \to + \infty}} \mu \big(\B \lambda_0 (\beta(m))\big) = l \ \  \ \ \ \ \ \ \ \ \ \]

\[ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \ \To \exists_{k \in I}\bigg(\bigcup_{n \in \Nat} \B \lambda_0 (\alpha(n)) = \B \lambda_0 (k)  \ \& \ \mu\big(\B \lambda_0 (k)\big) = l\bigg)\bigg]\bigg\}. \]

\[ (\CM_3) \ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \ \ \ \ \ \ \   \forall_{i, j \in I}\forall_{\B A(X) \in \Fam(\D 1, \B X)}\bigg(\B \lambda_0(i) \subseteq \B \alpha_0(0) \subseteq \B \lambda_0(j) \ \& \ \mu \big(\B \lambda_0 (i)\big) = \mu \big(\B \lambda_0 (j)\big) \ \ \ \ \ \ \ \ \  \]

\[ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \To \exists_{k \in I}\big(\B \alpha_0(0) = \B \lambda_0(k)\big)\bigg). \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \]

Regarding the completeness conditions and the space $\C M(X)$, we show the following.

Let $\C M(X) := (X, \delta_0 \D F(X, \D 2)(\B X), \mu^*_{x_0})$ be the measure space of
complemented detachable subsets of $X$.

$\C M(X)$ satisfies condition $(\CM_1)$.

The limited principle of omniscience $(\LPO)$ implies that $\C M(X)$ satisfies condition $(\CM_2)$.

In general, $\C M(X)$ does not satisfy condition $(\CM_3)$.

(i) Let $f \in \D F (X, \D 2)$, let $\B B := (B^1, B^0)$ be a given complemented subset of
$X$ with $\B \alpha_0 (0) := \B B$, and let $\delta_0^1 (f) \subseteq B^1$ and $\delta_0^0 (f)
\subseteq B^0$. Since $X = \delta_0^1 (f) \cup \delta_0^0 (f) \subseteq (B^1 \cup B^0) \subseteq X$,
we get $B^1 \cup B^0 = X$, and hence $\B B = \B \delta_0 (\chi_{\B B})$.

(ii) Let $\alpha, \beta : \Nat \to \D F(X, \D 2)$, and $l \in (0, + \infty)$ such that

\[ \forall_{m \in \Nat}\bigg(\bigcup_{n = 1}^m \B \delta_0 (\alpha_n) = \B \delta_0 (\beta_m)\bigg)
\ \& \  \exists  \lim_{\mathsmaller{m \to + \infty}} \beta_m (x_0) \ \& \ \lim_{\mathsmaller{m \to + \infty}}
\beta_m (x_0) = l. \]

The last conjunct is equivalent to $\exists_{m_0 \in \Nat}\forall_{m \geq m_0}\big(\beta_m (x_0) = l\big)$, and
since $\beta_m (x_0) \in \D 2$, we get $l \in \D 2$. For every $x \in X$ the sequence $n \mapsto
\alpha_n (x)$ is in $\D F(\Nat, \D 2)$, hence by $(\LPO)$ we define the function $f$ from $X$ to $\D 2$ by the rule

\[ f(x) := \left\{ \begin{array}{ll}
1    &\mbox{, $\exists_{n \in \Nat}\big(\alpha_n (x) = 1\big)$}\\
0             &\mbox{, $\forall_{n \in \Nat}\big(\alpha_n (x) = 0\big)$.}
\end{array}
\right.\]

By the definition of interior union and intersection it is immediate to show that

\[ \bigcup_{n \in \Nat} \B \delta_0 (\alpha_n) = \B \delta_0 (f)  \TOT
\bigcup_{n \in \Nat} \delta_0^1 (\alpha_n) = \delta_0^1 (f) \ \& \ \bigcap_{n \in \Nat}
\delta_0^0 (\alpha_n) = \delta_0^0 (f).\]

It remains to show that $f(x_0) = l$. If $l = 0$, then
$\exists_{m_0 \in \Nat}\forall_{m \geq m_0}\big(\beta_m (x_0) = 0\big)$, which implies that
$\forall_{n \in \Nat}\big(\alpha_n (x_0) = 0\big) : \TOT f(x_0) := 0$. If $l = 1$, then
$\exists_{m_0 \in \Nat}\forall_{m \geq m_0}\big(\beta_m (x_0) = 1\big)$, which implies that
$\exists_{n \in \{1, \ldots, m_0\}}\big(\alpha_n (x_0) = 1\big)  \To f(x_0) := 1$.

(iii) If $X := \D 3$, let $f : \D 3 \to \D 2$ be defined by $f(0) := 1, f(1) := 0 =: f(2)$ and
let $g \colon \D 3 \to \D 2$ be the constant function with value $1$. If
$\B B := \big(\{0\}, \{1\}\big)$, then $\delta_0^1 (f) := \{0\} = B^1 \subseteq
\delta_0^1 (g)$ and $\emptyset = \delta_0^0 (g) \subseteq B^0 \subseteq \delta_0^0 (f)$. If $x_0 := 0$,
then $\mu_0 (f) = \mu_0 (g)$, but $\B B$ cannot “pseudo-belong” to $\C D(\D 3)$, since $B^1 \cup B^0$
is a proper subset of $\D 3$.

§ REAL-VALUED PARTIAL FUNCTIONS

We present here all facts on real-valued partial functions necessary to the definition of an
integration space within $\BST$ (Definition <ref>).

If $(X, =_X, \neq_X)$ is an inhabited set, we denote by $f_A := (A, i_A^X, f_A^{\Real})$ a
real-valued partial function on $X$

(E) at (0,0) $A$;
[right=of E] (F) $X$;
[below=of F] (A) $\Real$.;

[right hook->] (E)–(F) node [midway,above] $i_A^X$;
[->] (E)–(A) node [midway,left] $f_A^{\Real} \ \ $;

We say that $f_A$ is strongly extensionalstrongly extensional partial function, if
$f_A^{\Real}$ is strongly extensional, where $A$ is equipped with its canonical inequality as a
subset of $X$ i.e., for every $a, a{'} \in A$

\[f_A^{\Real}(a) \neq_{\Real} f_A^{\Real}(a{'}) \To i_A^X(a) \neq_X i_A^X(a{'}).\]

Let $\C F(X) := \C F(X, \Real)$$\C F(X)$ be the class of partial functions
from $X$ to $\Real$, and $\C F^{\se}(X)$$\C F^{\se}(X)$ the class of strongly extensional
partial functions from $(X =_X, \neq_X)$ to $(\Real, =_{\Real}, \neq_{\Real})$.

Let $f_A := (A, i_A^X, f_A^{\Real}), f_B := (B, i_B^X, f_B^{\Real})$ in $\C F(X)$

(E) at (0,0) $A$;
[right=of E] (B) $X$;
[right=of B] (F) $B$;

[below=of B] (C) $\Real$.;

[right hook->] (E)–(B) node [midway,above] $i_A^X$;
[left hook->] (F)–(B) node [midway,above] $i_B^X$;
[->] (E)–(C) node [midway,left] $f_A^{\Real} \ \ $;
[->] (F)–(C) node [midway,right] $ \ f_B^{\Real}$;

If $\lambda \in \Real$, let $\lambda
f_A := (A, i_A^X, \lambda f_A^{\Real}) \in \C F(X)$$\lambda f_A$,$f_A \ \square \ f_B$ and
$ f_A \ \square \ f_B := \big(A \cap B, i_{A \cap B}^X, \big(f_A^{\Real} \ \square
\ f_B^{\Real}\big)_{A \cap B}^{\Real}\big)$,

\[ (f_A^{\Real} \ \square \ f_B^{\Real}\big)_{A \cap B}^{\Real} := f_A^{\Real}(a) \
\square \ f_B^{\Real}(b); \ \ \ \ (a, b) \in A \cap B, \  \ \square \in \{+, \cdot, \wedge, \vee\}.\]

The operation $(f_A^{\Real} \ \square \ f_B^{\Real}\big)_{A \cap B}^{\Real} \colon A \cap B \sto \Real$
is a function, as if $(a, b) =_{A \cap B} (a{'}, b{'}) :\TOT i_A^X =_X i_A^X(a{'})$,
and since $i_B^X(b) =_X i_A^X(a)$ and $i_B^X(b{'}) =_X i_A^X(a{'})$, we get $a =_A a{'}$, hence
$f_A^{\Real}(a) =_{\Real} f_A^{\Real}(a{'})$, and $b =_B b{'}$, hence $f_B^{\Real}(b) =_{\Real} f_B^{\Real}(b{'})$.
If $\lambda$ denotes also the constant function $\lambda \in \Real$ on $X$

(E) at (0,0) $A$;
[right=of E] (B) $X$;
[right=of B] (F) $X$;

[below=of B] (C) $\Real$,;

[right hook->] (E)–(B) node [midway,above] $i_A^X$;
[left hook->] (F)–(B) node [midway,above] $\id_X$;
[->] (E)–(C) node [midway,left] $f_A^{\Real} \ \ $;
[->] (F)–(C) node [midway,right] $ \ \lambda$;

we get as a special case the partial function $f_A \wedge \lambda := \big(A \cap X, i_{A \cap X}^X,
\big(f_A^{\Real} \wedge \lambda\big)_{A \cap X}^{\Real}\big)$, where $A \cap X := \{ (a, x) \in A \times X
\mid i_A^X(a) =_X x\}$, $i_{A \cap X}(a, x) := i_A^X(a)$, and $\big(f_A^{\Real} \wedge \lambda\big)_{A \cap X}^{\Real}(a,x) := f_A^{\Real}(a) \wedge \lambda(x) := f_A^{\Real}(a) \wedge \lambda$, for every $(a, x) \in A \cap X$.
By Definition <ref>, if $\Lambda(X,\Real) := (\lambda_0, \C E^X, \lambda_1, \C P^{\Real})
\in \Fam(I, X, \Real)$,
if $(i, j) \in D(I)$, the following diagram commutes

(E) at (0,0) $\lambda_0(i)$;
[right=of E] (B) ;
[right=of B] (F) $\lambda_0(j)$;

[below=of B] (A) $X$;
[below=of A] (C) $ \ \Real$,;

[->,bend left] (E) to node [midway,below] $\lambda_{ij}$ (F);
[->,bend left] (F) to node [midway,above] $\lambda_{ji}$ (E);
[->,bend right=50] (E) to node [midway,left] $f_i^{\Real}$ (C);
[->,bend left=50] (F) to node [midway,right] $f_j^{\Real}$ (C);
[right hook->,bend right=20] (E) to node [midway,left] $ \ \C E_i^X \ $ (A);
[left hook->,bend left=20] (F) to node [midway,right] $\ \C E_j^X \ $ (A);

\[ f_i := \big(\lambda_0(i), \C E_i^X, f_i^{\Real}\big) \in \C F(X), \ \ \ \
f_i^{\Real} := \C P^{\Real}_i \colon \lambda_0(i) \to \Real; \ \ \ \ i \in I.\]

If $f_i^{\Real}$ is strongly extensional, then, for every $u, w \in \lambda_0(i)$, we have that
$f_i^{\Real}(u) \neq_{\Real} f_i^{\Real}(w) \To \C E_i^X(u) \neq_X \C E_i^X(w)$.
As in Definition <ref>, If $\kappa \colon \Nat^+ \to I$, the family
$\Lambda(X, \Real) \circ \kappa := \big(\lambda_0 \circ \kappa, \C E^X \circ \kappa, \lambda_1
\circ \kappa, \C P^{\Real} \circ \kappa\big) \in \Fam(\Nat^+, X, \Real)$ is the $\kappa$-subsequence
of $\Lambda(X, \Real)$, where

\[ (\lambda_0 \circ \kappa)(n) := \lambda_0(\kappa(n)), \ \ \ \ \big(\C E^X \circ \kappa\big)_n :=
\C E_{\kappa(n)}^X, \ \  \ \ (\lambda_1 \circ \kappa)(n, n) := \lambda_{\kappa(n)\kappa(n)} :=
\id_{\lambda_0(\kappa(n))}, \]

\[  \big(\C P^{\Real} \circ \kappa\big)_n := \C P_{\kappa(n)}^{\Real} := f_{\kappa(n)}^{\Real}; \ \ \ \ n \in \Nat^+.\]

Let $\lambda_0I (X, \Real)$$\lambda_0I (X, \Real)$ be the totality $I$, and we write $f_i
\in \lambda_0I(X, \Real)$, instead of $i \in I$, as we define

\[ i =_{\lambda_0I (X, \Real)} j :\TOT f_i =_{\C F(X)} f_j.\]

If we consider the intersection $\bigcap_{n \in \Nat^+}(\lambda_0 \circ \kappa)(n) :=
\bigcap_{n \in \Nat^+}\lambda_0(\kappa(n))$,
by Definition <ref>

\[ \Phi \colon \bigcap_{n \in \Nat^+}\lambda_0(\kappa(n))  :\TOT \Phi \colon
\bigcurlywedge_{n \in \Nat^+}\lambda_0(\kappa(n)) \ \ \& \ \
\forall_{n, m \in \Nat^+}\big(\C E_{\kappa(n)}^X(\Phi_n) =_X \C E_{\kappa(m)}^X(\Phi_m)\big), \]

\[ \Phi =_{\mathsmaller{\bigcap_{n \in \Nat^+}\lambda_0(\kappa(n))}} \Theta
:\TOT \C E_{\kappa(1)}^X(\Phi_1) =_X \C E_{\kappa(1)}^X(\Theta_1), \]

\[ e_{\mathsmaller{\bigcap}}^{\Lambda(X, \Real) \circ \kappa} \colon
\bigcap_{n \in \Nat^+}\lambda_0(\kappa(n)) \eto X, \ \ \ \
e_{\mathsmaller{\bigcap}}^{\Lambda(X, \Real) \circ \kappa}(\Phi) :=
\big(\C E^X \circ \kappa)_1 (\Phi_1) := \C E_{\kappa(1)}^X(\Phi_1).\]

Let $\Lambda(X,\Real) := (\lambda_0, \C E^X, \lambda_1, \C P^{\Real}) \in
\Fam(I, X, \Real)$, $\kappa \colon \Nat^+ \to I$, and
$\Lambda(X, \Real) \circ \kappa$ the $\kappa$-subsequence of $\Lambda(X, \Real)$.
If $(A, i_A^{\mathsmaller{\bigcap}}) \subseteq \bigcap_{n \in \Nat^+}\lambda_0(\kappa(n))$, we define the function

\[ \sum_{n \in \Nat^+}^Af_{\kappa(n)}^{\Real} \colon A \to \Real, \ \ \ \
\bigg(\sum_{n \in \Nat^+}^Af_{\kappa(n)}^{\Real}\bigg)(a)
:= \sum_{n \in \Nat^+}f_{\kappa(n)}^{\Real}\bigg(\big[i_A^{\mathsmaller{\bigcap}}(a)\big]_n\bigg); \ \ \ \ a \in A,\]

under the assumption that the series on the right converge in $\Real$, for every $a \in \Real$.

In the special case
$\bigcap_{n \in \Nat^+}\lambda_0(\kappa(n)), id_{\mathsmaller{\bigcap_{n \in \Nat^+}\lambda_0(\kappa(n))}})
\subseteq \bigcap_{n \in \Nat^+}\lambda_0(\kappa(n))$, we get the function

\[ \sum_{n \in \Nat^+}^{\mathsmaller{\bigcap}}f_{\kappa(n)}^{\Real} \colon
\bigcap_{n \in \Nat^+}\lambda_0(\kappa(n)) \to \Real, \ \ \ \
\bigg(\sum_{n \in \Nat^+}^{\mathsmaller{\bigcap}}f_{\kappa(n)}^{\Real}\bigg)(\Phi)
:= \sum_{n \in \Nat^+}f_{\kappa(n)}^{\Real}\big(\Phi_n\big); \ \ \ \
\Phi \in \bigcap_{n \in \Nat^+}\lambda_0(\kappa(n)),\]

under the assumption on the convergence of the corresponding series.

If in Definition <ref> the partial functions $f_{\kappa(n)} :=
\big(\lambda_0(\kappa(n)), \C E_{\kappa(n)}^X, f_{\kappa(n)}^{\Real}\big)$ are strongly extensional,
for every $n \in \Nat^+$, then the real-valued partial function

(E) at (0,0) $A$;
[right=of E] (G) $\bigcap_{n \in \Nat^+}\lambda_0(\kappa(n))$;
[right=of G] (H) ;
[right=of H] (F) $X$;
[below=of F] (A) $\Real$;

[right hook->] (E)–(G) node [midway,above] $i_A^{\mathsmaller{\bigcap}}$;
[right hook->] (G)–(F) node [midway,above] $e_{\mathsmaller{\bigcap}}^{\Lambda(X, \Real) \circ \kappa} $;
[right hook->,bend right=20] (E) to node [midway,above] $ \ \ \ \ \
\sum_{n \in \Nat^+}^Af_{\kappa(n)}^{\Real}  $ (A);

\[ f_A := \bigg(A, \ e_{\mathsmaller{\bigcap}}^{\Lambda(X, \Real) \circ \kappa}
\circ i_A^{\mathsmaller{\bigcap}}, \ \sum_{n \in \Nat^+}^Af_{\kappa(n)}^{\Real} \bigg)\]

is strongly extensional.

Let $a, a{'} \in A$ such that

\[ \bigg(\sum_{n \in \Nat^+}^Af_{\kappa(n)}^{\Real}\bigg)(a) := l \neq_{\Real} l{'} :=
\bigg(\sum_{n \in \Nat^+}^Af_{\kappa(n)}^{\Real}\bigg)(a{'}).\]

There is $N \in \Nat^+$ such that, if $\varepsilon := |l - l{'}| >0$, then

\begin{align*}
\varepsilon & \leq \bigg| l - \sum_{n = 1}^Nf_{\kappa(n)}^{\Real}\bigg(\big[i_A^{\mathsmaller{\bigcap}}(a)\big]_n\bigg)
\bigg| +
\bigg| \sum_{n = 1}^Nf_{\kappa(n)}^{\Real}\bigg(\big[i_A^{\mathsmaller{\bigcap}}(a)\big]_n\bigg) -
\sum_{n = 1}^Nf_{\kappa(n)}^{\Real}\bigg(\big[i_A^{\mathsmaller{\bigcap}}(a{'})\big]_n\bigg) \bigg| \\
& \ \ \ \ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  +
\bigg| \sum_{n = 1}^Nf_{\kappa(n)}^{\Real}\bigg(\big[i_A^{\mathsmaller{\bigcap}}(a{'})\big]_n\bigg) - l{'}\bigg|\\
& \leq \frac{\varepsilon}{4} +
\bigg| \sum_{n = 1}^Nf_{\kappa(n)}^{\Real}\bigg(\big[i_A^{\mathsmaller{\bigcap}}(a)\big]_n\bigg) -
\sum_{n = 1}^Nf_{\kappa(n)}^{\Real}\bigg(\big[i_A^{\mathsmaller{\bigcap}}(a{'})\big]_n\bigg) \bigg| +
\frac{\varepsilon}{4} \To
\end{align*}

\begin{align*}
0 & < \bigg| \sum_{n = 1}^Nf_{\kappa(n)}^{\Real}\bigg(\big[i_A^{\mathsmaller{\bigcap}}(a)\big]_n\bigg) -
\sum_{n = 1}^Nf_{\kappa(n)}^{\Real}\bigg(\big[i_A^{\mathsmaller{\bigcap}}(a{'})\big]_n\bigg) \bigg|\\
& = \bigg| \sum_{n = 1}^N \bigg[f_{\kappa(n)}^{\Real}\bigg(\big[i_A^{\mathsmaller{\bigcap}}(a)\big]_n\bigg) -
f_{\kappa(n)}^{\Real}\bigg(\big[i_A^{\mathsmaller{\bigcap}}(a{'})\big]_n\bigg)\bigg] \bigg|\\
& \leq \sum_{n = 1}^N \bigg| f_{\kappa(n)}^{\Real}\bigg(\big[i_A^{\mathsmaller{\bigcap}}(a)\big]_n\bigg) -
\end{align*}

By the property of positive real numbers $x + y > 0 \To [x > 0 \vee y > 0$ (see [20], p. 13), then

\[ 0 < \bigg| f_{\kappa(n)}^{\Real}\bigg(\big[i_A^{\mathsmaller{\bigcap}}(a)\big]_n\bigg) -

for some $n \in \Nat^+$ with $1 \leq n \leq N$. Since $f_{\kappa(n)}^{\Real}$ is strongly extensional,
by Definition <ref>

\[ \C E_{\kappa(1)}^X\bigg(\big[i_A^{\mathsmaller{\bigcap}}(a)\big]_1\bigg) =_X
\C E_{\kappa(n)}^X\bigg(\big[i_A^{\mathsmaller{\bigcap}}(a)\big]_n\bigg) \neq_X
\C E_{\kappa(n)}^X\bigg(\big[i_A^{\mathsmaller{\bigcap}}(a{'})\big]_n\bigg) =_X
\C E_{\kappa(1)}^X\bigg(\big[i_A^{\mathsmaller{\bigcap}}(a{'})\big]_1\bigg),\]

which is the required canonical equality of $a, a{'}$ in $A$ as a subset of $X$.

Clearly, we have that (see Definition <ref>)

(E) at (0,0) $A$;
[right=of E] (B) ;
[right=of B] (F) $\bigcap_{n \in \Nat^+}\lambda_0(\kappa(n))$;

[below=of B] (A) $X$;
[below=of A] (C) $ \ \Real$;

[right hook->] (E) to node [midway,above] $i_A^{\mathsmaller{\bigcap}}$ (F);

[->,bend right=70] (E) to node [midway,left] $\sum_{n \in \Nat^+}^Af_{\kappa(n)}^{\Real} $ (C);
[->,bend left=70] (F) to node [midway,left] $\sum_{n \in \Nat^+}^{\mathsmaller{\bigcap}}f_{\kappa(n)}^{\Real} \ \ $ (C);
[right hook->,bend right=40] (E) to node [midway,right] $ \ \mathsmaller{e_{\mathsmaller{\bigcap}}^{\Lambda(X, \Real) \circ \kappa} \circ i_A^{\mathsmaller{\bigcap}}}$ (A);
[left hook->,bend left=40] (F) to node [midway,right] $\mathsmaller{e_{\mathsmaller{\bigcap}}^{\Lambda(X, \Real) \circ \kappa}}$ (A);

\[ \bigg(A, \ e_{\mathsmaller{\bigcap}}^{\Lambda(X, \Real) \circ \kappa} \circ
i_A^{\mathsmaller{\bigcap}}, \ \sum_{n \in \Nat^+}^Af_{\kappa(n)}^{\Real} \bigg)
\leq \bigg(\bigcap_{n \in \Nat^+}\lambda_0(\kappa(n)),
\ e_{\mathsmaller{\bigcap}}^{\Lambda(X, \Real) \circ \kappa}, \
\sum_{n \in \Nat^+}^{\mathsmaller{\bigcap}}f_{\kappa(n)}^{\Real} \bigg).\]

§ INTEGRATION AND PRE-INTEGRATION SPACES

Next we reformulate predicatively the Bishop-Cheng definition of an integration space
(see Note <ref> to compare it with the original definition).

Let $(X, =_X, \neq_X)$ be an inhabited set, $\Lambda(X,\Real) :=
(\lambda_0, \C E^X, \lambda_1, \C P^{\Real}) \in \Fam(I, X, \Real)$, such that $f_i :=
\big(\lambda_0(i), \C E_i^X, f_i^{\Real}\big)$ is strongly extensional, for every $i \in I$,
let $\lambda_0I (X, \Real)$ be the totality $I$, equipped with the equality $i =_{\lambda_0I (X, \Real)} j
:\TOT f_i =_{\C F(X)} f_j$, for every $i \in I$, and let a mapping

\[ \int \colon \lambda_0I (X, \Real) \to \Real, \ \ \ \ f_i \mapsto \int f_i; \ \ \ \ i \in I,\]

such that the following conditions hold:

\[(\IS_1) \ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \ \ \forall_{i \in I}\forall_{a \in \Real}\exists_{j \in I}\bigg(a f_i =_{\C F(X)} f_j \ \ \& \ \ \int f_j =_{\Real} a \int f_i\bigg). \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \]

\[(\IS_2) \ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \ \ \forall_{i, j \in I}\exists_{k \in I}\bigg(f_i + f_j =_{\C F(X)} f_k \  \ \& \ \ \int f_k =_{\Real} \int f_i\ + \int f_j\bigg). \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \]

\[(\IS_3) \ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \ \ \forall_{i \in I}\exists_{j \in I}\big( |f_i| =_{\C F(X)} f_j \big). \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \   \]

\[(\IS_4) \ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \ \ \forall_{i \in I}\exists_{j \in I}\big( f_i \wedge 1 =_{\C F(X)} f_j \big). \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \   \]

\[(\IS_5) \  \ \ \ \  \ \ \ \ \ \ \ \ \  \ \ \ \ \ \ \ \  \forall_{i \in I}\forall_{\kappa \in \D F(\Nat^+, I)}\bigg\{\bigg[\sum_{n \in \Nat^+}\int f_{\kappa(n)} \in \Real \  \ \& \ \sum_{n \in \Nat^+}\int f_{\kappa(n)} < \int f_i\bigg] \To  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \]

\[ \exists_{(\Phi, u) \ \in \ \big(\bigcap_{n \in \Nat^+}\lambda_0(\kappa(n)) \big)\ \cap \ \lambda_0(i)}\bigg( \bigg(\sum_{n \in \Nat^+}^{\mathsmaller{\bigcap}}f_{\kappa(n)}\bigg)(\Phi) := \sum_{n \in \Nat^+}f_{\kappa(n)}^{\Real}(\Phi_n) \in \Real \  \ \& \ \]

\[ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \sum_{n \in \Nat^+}f_{\kappa(n)}^{\Real}(\Phi_n) < f_i^{\Real}(u). \bigg)\bigg\}\]

\[(\IS_6) \ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \ \ \ \ \ \ \  \ \ \exists_{i \in I}\bigg( \int  f_i =_{\Real} 1 \bigg). \ \ \ \ \ \ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \   \]

\[(\IS_7) \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \ \ \ \  \forall_{i \in I}\forall_{\alpha \in \D F(\Nat^+, I)}\bigg(\forall_{n \in \Nat^+}\bigg(n \bigg(\frac{1}{n} f_i \ \wedge \ 1\bigg) =_{\C F(X)} f_{\alpha(n)}\bigg) \To \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \]

\[ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \lim_{\mathsmaller{n \longrightarrow +\infty}} \int f_{\alpha(n)} \in \Real \ \ \& \
\lim_{\mathsmaller{n \longrightarrow +\infty}} \int f_{\alpha(n)} =_{\Real} \int f_i\bigg). \ \ \ \ \ \ \ \ \ \ \ \ \]

\[(\IS_8) \ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \ \ \ \ \ \ \ \ \ \ \  \forall_{i \in I}\forall_{\alpha \in \D F(\Nat^+, I)}\bigg(\forall_{n \in \Nat^+}\bigg(\frac{1}{n}\big(n |f_i| \ \wedge \ 1\big) =_{\C F(X)} f_{\alpha(n)}\bigg) \To \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \]

\[ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \lim_{\mathsmaller{n \longrightarrow +\infty}} \int f_{\alpha(n)} \in \Real  \ \ \& \  \lim_{\mathsmaller{n \longrightarrow +\infty}} \int f_{\alpha(n)} =_{\Real} 0\bigg). \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \]

We call the triplet $\C L := (X, \lambda_0I (X, \Real), \int)$ an integration spaceintegration space.

In the formulation of $(\IS_5)$ we have that

\[ \bigg(\bigcap_{n \in \Nat^+}\lambda_0(\kappa(n))\bigg) \cap  \lambda_0(i)
:= \bigg\{(\Phi, u) \in \bigg(\bigcap_{n \in \Nat^+}\lambda_0(\kappa(n))\bigg) \times
\lambda_0(i) \ \mathlarger{\mathlarger{\mid}} \ \C E^X_{\kappa(1)}(\Phi) =_X \C E_i^X(u)\bigg\},\]

(E) at (0,0) $\lambda_0(\kappa(n))$;
[right=of E] (B) $X$;
[right=of B] (F) $\lambda_0(i)$;

[below=of B] (C) $\Real$.;

[right hook->] (E)–(B) node [midway,above] $\C E_{\kappa(n)}^X$;
[left hook->] (F)–(B) node [midway,above] $\C E_i^X$;
[->] (E)–(C) node [midway,left] $f_{\kappa(n)}^{\Real} \ \ $;
[->] (F)–(C) node [midway,right] $ \ f_i^{\Real}$;

If, for every $a \in \Real$, such that $a > 0$, and every $i \in I$, we define

\[ f_i \ \wedge \ a := a \bigg(\frac{1}{a} f_i \ \wedge \ 1\bigg),\]

the formulation of $(\IS_7)$ and $(\IS_8)$ becomes, respectively,

\[ \forall_{i \in I}\forall_{\alpha
\in \D F(\Nat^+, I)}\bigg(\forall_{n \in \Nat^+}\big(f_i \ \wedge \ n =_{\C F(X)}
f_{\alpha(n)}\big) \To \lim_{\mathsmaller{n \longrightarrow +\infty}} \int f_{\alpha(n)}
=_{\Real} \int f_i\bigg),  \]

\[ \forall_{i \in I}\forall_{\alpha \in \D F(\Nat^+, I)}\bigg(\forall_{n \in \Nat^+}\bigg(|f_i| \ \wedge \
\frac{1}{n}\bigg) =_{\C F(X)} f_{\alpha(n)}\bigg) \To \lim_{\mathsmaller{n \longrightarrow +\infty}}
\int f_{\alpha(n)} =_{\Real} 0\bigg),  \]

where, for simplicity, we skip to mention he existence of the corresponding limits in $\Real$.
We also quantify over $\D F(\Nat^+, I)$, in order to avoid the use of countable choice. If we had written
in its premise the formula $\forall_{n \in \Nat^+}\exists_{j \in I}\big(f_i \ \wedge \ n =_{\C F(X)} f_j\big)$,
we would need countable choice ($\Nat{-}I$) to generate a sequence in $I$ to describe the limit of the
corresponding integrals. Moreover, by $(\IS_1)$, $(\IS_3)$ and $(\IS_4)$, and the definition of $f \wedge a $
above we get  $\forall_{i \in I}\forall_{a \in \Real^+}\exists_{j \in I}\big(f_i \wedge  a =_{\C F(X)} f_j\big)$.

Let $(X, =_X, \neq_X)$ be an inhabited set, and let the set $(I, =_I)$ be equipped with
operations $\cdot_a \colon I \sto I$, for every $a \in \Real$, $+ \colon I \times I \sto I$, $|.| \colon I \sto I$,
and $\wedge_1 \colon I \sto I$, where

\[ \cdot_a(i) := a \cdot i, \ \ \ \ +(i,j) := i + j, \ \ \ \ |.|(i) := |i|; \ \ \ \ i \in I, \ a \in \Real.\]

Let also the operation $\wedge_a \colon I \sto I$, defined by the previous operations with the rule

\[ \wedge_a := \cdot_a \circ \wedge_1 \circ \cdot_{a^{-1}}; \ \ \ \ a \in \Real \ \& \ a > 0.\]

Let $\Lambda(X,\Real) := (\lambda_0, \C E^X, \lambda_1, \C P^{\Real}) \in \Set(I, X, \Real)$ i.e.,
$f_i =_{\C F(X)} f_j \To i =_I j$, for every $i, j \in I$, and $f_i := \big(\lambda_0(i),
\C E_i^X, f_i^{\Real}\big)$ is strongly extensional, for every $i \in I$. Let also a mapping

\[ \int \colon I \to \Real, \ \ \ \ i \mapsto \int i; \ \ \ \ i \in I,\]

such that the following conditions hold:

\[(\PIS_1) \ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \ \ \forall_{i \in I}\forall_{a \in \Real}\bigg(a f_i =_{\C F(X)} f_{a \cdot i} \ \ \& \ \ \int a \cdot i =_{\Real} a \int i\bigg). \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \]

\[(\PIS_2) \ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \ \ \forall_{i, j \in I}\bigg(f_i + f_j =_{\C F(X)} f_{i + j} \  \ \& \ \ \int (i + j) =_{\Real} \int i \ + \int j\bigg). \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \]

\[(\PIS_3) \ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \ \ \forall_{i \in I}\big( |f_i| =_{\C F(X)} f_{|i|} \big). \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \   \]

\[(\PIS_4) \ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \ \ \forall_{i \in I}\big( f_i \wedge 1 =_{\C F(X)} f_{\wedge_1(i)} \big). \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \   \]

\[(\PIS_5) \  \ \ \ \  \ \ \ \ \ \ \ \ \  \ \ \ \ \ \ \ \  \forall_{i \in I}\forall_{\kappa \in \D F(\Nat^+, I)}\bigg\{\bigg[\sum_{n \in \Nat^+}\int \kappa(n) \in \Real \  \ \& \ \sum_{n \in \Nat^+}\int \kappa(n) < \int i\bigg] \To  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \]

\[ \exists_{(\Phi, u) \ \in \ \big(\bigcap_{n \in \Nat^+}\lambda_0(\kappa(n)) \big)\ \cap \ \lambda_0(i)}\bigg( \bigg(\sum_{n \in \Nat^+}^{\mathsmaller{\bigcap}}f_{\kappa(n)}\bigg)(\Phi) := \sum_{n \in \Nat^+}f_{\kappa(n)}^{\Real}(\Phi_n) \in \Real \  \ \& \ \]

\[ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \sum_{n \in \Nat^+}f_{\kappa(n)}^{\Real}(\Phi_n) < f_i^{\Real}(u). \bigg)\bigg\}\]

\[(\PIS_6) \ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \ \ \ \ \ \ \  \ \ \exists_{i \in I}\bigg( \int  i =_{\Real} 1 \bigg). \ \ \ \ \ \ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \   \]

\[(\PIS_7) \ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \ \   \forall_{i \in I}\bigg(\lim_{\mathsmaller{n \longrightarrow +\infty}} \int \wedge_n(i) \in \Real \ \ \& \ \lim_{\mathsmaller{n \longrightarrow +\infty}} \int \wedge_n(i) =_{\Real} \int i\bigg). \  \ \ \ \ \ \ \ \ \ \ \  \ \ \ \ \ \ \ \ \ \ \]

\[(\PIS_8) \ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \ \   \forall_{i \in I}\bigg(\lim_{\mathsmaller{n \longrightarrow +\infty}} \int \wedge_{\frac{1}{n}}(|i|) \in \Real \ \ \& \ \lim_{\mathsmaller{n \longrightarrow +\infty}} \int \wedge_{\frac{1}{n}}(|i|) =_{\Real} 0\bigg). \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \   \]

We call the triplet $\C L_0 := (X, I, \int)$ a pre-integration spacepre-integration space.

All the operations on $I$ defined above are functions. E.g., since $\Lambda(X, \Real)  \in \Set(I, X, \Real)$,

\[ i =_I i{'} \To f_i =_{\C F(X)} f_{i{'}} \To a f_i =_{\C F(X)} a f_{i{'}} \To f_{a \cdot i}
=_{\C F(X)} f_{a{'} \cdot i} \To a \cdot i =_I a{'} \cdot i.\]

It is immediate to see that a pre-integration space induces an integration space, if

\[ \forall_{i \in I}\forall_{a \in \Real^+}\big(f_i \ \wedge \ a  =_{\C F(X)} f_j \To \wedge_a(i) =_I j\big),\]

and hence $(\PIS_7)$ and $(\PIS_8)$ imply $(\IS_7)$ and $(\IS_8)$, respectively, with the integral

\[ \int^* f_i := \int i; \ \ \ \ i \in I.\]

The notion of a pre-integration space is simpler than that of an integration space, and also closer
to the Bishop-Cheng notion of an integration space. One could say that a pre-integration space is the
“right” notion of integration space within $\BST$. In [18], p. 52 Bishop and Cheng  formulate
the non-trivial theorem that a measure space induces the integration space of the corresponding simple
functions (see also [19], p. 285). In [132] Zeuner interpreting the various constructions
of Bishop and Cheng into the framework of pre-measure and pre-integration
spaces[The notion of pre-measure space used in [132], which is a bit
different from the one included here, is an appropriate copy of Bishop's definition of a measure space given
in [9] (see Note <ref>).] gave a proof of this theorem within $\BST$. Here we only
sketch this construction.

Let $\B \Lambda(X) := \big(\lambda_0^1, \C E^{1,X}, \lambda_1^1, \lambda_0^0, \C E^{0,X},
\lambda_1^0) \in \Fam(I, \B X)$
and $i_0 \in I$. To each $i \in I$ corresponds the real-valued partial function

\[ \chi_i := \big(\lambda_0^1(i) \cup \lambda_0^0(i), \C E_i^X, \chi_i^{\Real}\big) \in \C F(X), \]

(E) at (0,0) $ \lambda_0^1(i) \cup \lambda_0^0(i)$;
[right=of E] (F) $X$;
[below=of F] (B) $\lambda_0^0(i)$;
[above=of F] (D) $\lambda_0^1(i)$;
[below=of B] (C) $\Real$.;

[right hook->] (E)–(F) node [midway,above] $\C E_i^X$;
[->] (E)–(C) node [midway,left] $\chi_i^{\Real} \ \ $;
[right hook->] (D)–(F) node [midway,right] $\C E_i^{0,X}$;
[left hook->] (B)–(F) node [midway,right] $\C E_i^{1,X}$;
[left hook->] (B)–(E) node [midway,right] $ \ \id$;
[right hook->] (D)–(E) node [midway,left] $\id \ $;

where $\C E_i^X$ is the canonical embedding of $\lambda_0^1(i) \cup \lambda_0^0(i)$ into $X$,
and $\chi_i^{\Real}$ is given by the rule of the partial function $\chi_{\B \lambda_0(i)}$.
The symbol $\id$ in the above diagram denotes the corresponding function defined by the identity-map rule.
If $m, n \in \Nat^+$, $i_1, \ldots, i_n, j_1, \ldots, j_m \in I$, and $a_{1_i}, \ldots a_{i_n}, b_1,
\ldots, b_m \in \Real$, the equality of the following real-valued partial functions is given by the commutativity
of the following diagram

\[ \sum_{k = 1}^n a_{i_k} \chi_{i_k} := \bigg( \bigcap_{k = 1}^n \big(\lambda_0^1(i_k) \cup
\lambda_0^0(i_k)\big), i^X_{\mathsmaller{\bigcap_{k = 1}^n (\lambda_0^1(i_k) \cup \lambda_0^0(i_k))}},
\ \sum_{k = 1}^n a_{i_k}\chi_{i_k}^{\Real}\bigg) \in \C F(X),\]

\[ \sum_{l = 1}^m b_{j_l} \chi_{j_l} := \bigg( \bigcap_{l = 1}^m \big(\lambda_0^1(j_l) \cup
\lambda_0^0(j_l)\big), i^X_{\mathsmaller{\bigcap_{l = 1}^m (\lambda_0^1(j_l) \cup \lambda_0^0(j_l)}},
\ \sum_{l = 1}^m b_{j_l}\chi_{j_l}^{\Real}\bigg) \in \C F(X),\]

(E) at (0,0) $\bigcap_{k = 1}^n \big(\lambda_0^1(i_k) \cup \lambda_0^0(i_k)\big)$;
[right=of E] (B) ;
[right=of B] (F) $\bigcap_{l = 1}^m \big(\lambda_0^1(j_l) \cup \lambda_0^0(j_l)\big)$;

[below=of B] (A) $X$;
[below=of A] (C) $ \ \Real$,;

[->,bend left] (E) to node [midway,below] $e$ (F);
[->,bend left] (F) to node [midway,above] $e{'}$ (E);
[->,bend right=50] (E) to node [midway,left] $\sum_{k = 1}^n a_{i_k}\chi_{i_k}^{\Real} \ $ (C);
[->,bend left=50] (F) to node [midway,right] $ \ \sum_{l = 1}^m b_{j_l}\chi_{j_l}^{\Real}$ (C);
[right hook->,bend right=20] (E) to node [midway,left] $ \mathsmaller{\mathsmaller{i^X_{\mathsmaller{\bigcap_{k = 1}^n (\lambda_0^1(i_k) \cup \lambda_0^0(i_k))}}}} \ $ (A);
[left hook->,bend left=20] (F) to node [midway,right] $\ \ \ \mathsmaller{\mathsmaller{ i^X_{\mathsmaller{\bigcap_{l = 1}^m (\lambda_0^1(j_l) \cup \lambda_0^0(j_l))}}}} $ (A);

for some (unique up to equality) functions $e$ and $e{'}$. If $\mu_0 \colon \Nat^+ \sto \D V_0$ is defined by
the rule $\mu_0(n) := (\Real \times I)^n$, for every $n \in \Nat^+$, and if the corresponding dependent
operation $\mu_1$ is defined in the obvious way, let the totality

\[ S(I, \B \Lambda(X)) := \sum_{n \in \Nat^+}(\Real \times I)^n, \]

\[(n, u) =_{S(I, \B \Lambda(X))} (m, w) :\TOT \sum_{k = 1}^n a_{i_k} \chi_{i_k}
=_{\C F(X)} \sum_{l = 1}^m b_{j_l} \chi_{j_l};,\]

where $u := \big((a_1, i_1), \ldots, (a_n, i_n)\big)$ and $w := \big((b_1, j_1), \ldots, (b_m, j_m)\big)$.
The family of simple functionsfamily of simple functions generated by the family $\B \Lambda (I, \B X)$
of complemented subsets of $X$ is the structure
$\Delta (X, \Real) := \big(\dom_0, \C Z^X, \dom_1, \C P^{\Real}\big) \in \Fam\big(S(I, \B \Lambda(X), X, \Real \big)$,
where $\dom_0 \colon S(I, \B \Lambda(X)) \sto \D V_0$ is defined by the rule

\[ \dom_0 (n, u) := \bigcap_{k = 1}^n \big(\lambda_0^1(i_k) \cup \lambda_0^0(i_k)\big);  \ \ \ \ u
:= \big((a_1, i_1), \ldots, (a_n, i_n)\big), \ n \in \Nat^+, \]

the embedding $\C Z^X_{n, u} \colon \dom_0(n, u) \eto X$ is defined in a canonical way through the embeddings
$\C E_{i_k}^{1,X}$ and $\C E_{i_k}^{0,X}$, where $k \in \{1, \ldots, n\}$.

If $(n, u) =_{S(I, \B \Lambda(X))} (m, w)$,
the mapping $\dom_{(n, u)(m, w)} \colon \dom_0(n, u) \to \dom_0(m, w)$ is defined, in order to avoid choice, as
the mapping $E_{(n,u)(m,w)}$, where $E$ is a modulus of equality for $D(S(I, \B \Lambda(X)))$
with $E_{(n,u)(n,u)} := \id_{\dom_0(n, u)}$, for every $(n,u) \in S(I, \B \Lambda(X))$. The fact that
$\Delta (X, \Real) \in \Set\big(S(I, \B \Lambda(X), X, \Real \big)$ is immediate to show. Hence,
to every $(n, u) \in  S(I, \B \Lambda(X))$ corresponds the partial function

\[ s_{(n,u)} := \bigg(\dom_0(n, u), \C Z^X_{(n, u)},  \sum_{k = 1}^n a_{i_k}\chi_{i_k}^{\Real}\bigg)
\in \C F(X); \ \ \ \ u := \big((a_1, i_1), \ldots, (a_n, i_n)\big). \]

If $\C M (\B \Lambda(X)) := (X, I, \mu)$ is a pre-measure space, then $\C M (\B \Lambda(X))$ induces
the pre-integration space $\C L(\B \Lambda(X)) := (X, S(I, \B \Lambda(X)), \int_{\mu})$, where

\[ \int_{\mu} \colon S(I, \B \Lambda(X)) \to \Real, \ \ \ \ (n, u) \mapsto \int_{\mu} (n, u),\]

\[ \int_{\mu} (n, u) := \sum_{k = 1}^n a_k \mu(i_k); \ \ \ \ u := \big((a_1, i_1), \ldots, (a_n, i_n)\big).\]

The many steps of this involved proof of Bishop and Cheng, appropriately translated into the
predicative framework of $\BST$, are found in [132], pp. 34–45.

§ NOTES

The set of Borel sets generated by a given family of complemented subsets of a set $X$, with respect
to a set $\Phi$ of real-valued functions on $X$, was introduced in [9], p. 68. This set is
inductively defined and plays a crucial role in providing important examples of measure spaces in Bishop's
measure theory developed in [9]. As this measure theory was replaced in [19] by the
Bishop-Cheng measure theory, an enriched version of [18] that made no use of Borel sets, the Borel
sets were somehow “forgotten” in the constructive literature.
In the introduction of [18], Bishop and Cheng explained why they consider their new measure
theory “much more natural and powerful theory”. They do admit though, that some results are harder
to prove (see [18], p. v). As it is also noted in [122], p. 25, the Bishop-Cheng measure
theory is highly impredicative, while Bishop's measure theory in [9] is highly predicative.
This fact makes the original Bishop-Cheng measure theory hard to implement in some functional-programming
language, a serious disandvantage from the computational point of view. This is maybe why, later attempts
to develop constructive measure theory were done within an abstract algebraic framework
(see [38], [41] and [123]).
Despite the above history of measure theory within Bishop-style constructive mathematics the set of
Borel sets is interestingly connected to the theory of Bishop spaces.

The definition of $\Borel(\B \Lambda(X))$ is given by Bishop in [9], p. 68, although a
rough notion of a family of complemented subsets is used, condition $(\Borel_3)$ is not mentioned,
and $F$ is an arbitrary subset of $\D F(X)$, and not necessarily a Bishop topology.
If we want to avoid the extensionality of $\Borel(\B \Lambda(X))$, we need to introduce a “pseudo”-membership
\[ \B A \ \dot {\in} \ \Borel(\B \Lambda(X))
:\TOT \exists_{\B B \in \Borel(\B \Lambda(X))}\big(\B A =_{\C P^{\Disj_F}(X)} \B B\big). \]

A similar condition is necessary, if we want to avoid extensionality in the definition the
least Bishop topology $\bigvee F_0$. Such an approach though, is not practical, and not compatible
to the standard practice to study extensional subsets of sets. The quantification over $\Fam(\D 1, F, \B X)$
is not equivalent to the quantification over the class $\C P^{\Disj_F}(X)$, as in order to define a family
in $\Fam(\D 1, F, \B X)$, we need to have already constructed an $F$-complemented subset of $X$.
I.e., an element of $\Fam(\D 1, F, \B X)$ is generated by an already constructed, or given element of
$\C P^{\Disj_F}(X)$, and not from an abstract element of it. Recall that we never define an assignment
routine from a class, like $\C P^{\Disj_F}(X)$, to a set like $\Fam(\D 1, F, \B X)$.

The notion of a least Bishop topology generated by a given set of function from $X$ to $\Real$,
together with the set of Borel sets generated by a family of complemented subsets of $X$, are the main
two inductively defined concepts found in [9]. The difference between the two inductive
definitions is non-trivial. The first is the inductive definition of a subset of $\D F(X)$, while
the second is the inductive definition of a subset of the class $\C P^{\Disj_F}(X)$.

As Bishop remarks in [9], p. 69, the proof of Proposition <ref>(iii) rests on the
property of $F$ that $\big(\frac{1}{n} - f\big) \in F$, for every $f \in F$ and $n \geq 1$. If we
define similarly the Borel sets generated by any set of real-valued functions $\Theta$ on $X$, then we
can find $\Theta$ such that $\Borel(\Theta)$ is closed under complements without satisfying the condition
$f \in \Theta \To \big(\frac{1}{n} - f \big)\in \Theta$. Such a set is $\D F (X, \D 2)$.  In this case we have that

\[ \B o_{\D F (X, \D 2)} (f) := \big([f = 1], [f = 0]\big) \ \ \ \& \ \ - \B o_{\D F (X, \D 2)} (f) =
\B o_{\D F (X, \D 2)}(1 - f). \]

Hence, the property mentioned by Bishop is sufficient, but not necessary.

A measure space is defined in [19], p. 282, and a complete measure space in [19], p. 289.
These definitions appeared first in [18] p. 47 and p. 55, respectively[In [18], p. 55,
condition $(\BCM_1)$ appears in the equivalent form: if $B$ is an element of $M$ such that
$B^1 \subseteq A^1$ and $B^0 \subseteq A^0$, then $A \in M$, where we have used the terminology that
corresponds to the formulation of $(\BCM_1)$ in the definition of Bishop-Cheng.].

Bishop-Cheng definition of a measure space.
A measure space is a triplet $(X, M, \mu)$ consisting of a nonvoidBishop-Cheng measure space
set $X$ with an inequality $\neq$, a set $M$ of complemented sets in
$X$, and a mapping $\mu$ of $M$ into $\Real^{0+}$, such that the following properties

$(\BCMS_1)$ If $A$ and $B$ belong to $M$, then so do $A \vee B$ and $A \wedge B$, and
$\mu(A) + \mu(B) = \mu(A \vee B) + \mu(A \wedge B)$.

$(\BCMS_2)$ If $A$ and $A \wedge B$ belong to $M$, then so does $A - B$, and $\mu(A)
= \mu(A \wedge B) + \mu(A - B)$.

$(\BCMS_3)$ There exists $A$ in $M$ such that $\mu(A) >0$.

$(\BCMS_4)$ If $(A_n)$ is a sequence of elements of $M$ such that $\lim_{k \to \infty}
\mu\big(\bigwedge_{n = 1}^k A_n\big)$ exists and is positive, then $\bigcap_{n}A_n^1$ is nonvoid.

We then call $\mu$ the measure, and the elements of $M$ the integrable sets, of the
measure space $(X, M, \mu)$. For each $A$ in $M$ the nonnegative number $\mu(A)$ is called
the measure of $A$.

Bishop-Cheng definition of a complete measure space. A measure space $(X, M, \mu)$ is
complete if the following three conditions hold.

$(\BCCMS_1)$ If $A$ is a complemented set, and $B$ is an element of $M$ suchBishop-Cheng complete measure space
that $\chi_A = \chi_B$ on $B^1 \cup B^0$, then $A \in M$.

$(\BCCMS_2)$ If $(A_n)$ is a sequence of elements of $M$ such that

$$l := \lim_{N \to \infty}\mu \bigg(\bigvee_{n = 1}^N A_n\bigg)$$

exists, then $\bigvee_n A_n$ belongs to $M$ and has measure $l$.

$(\BCCMS_3)$ If $A$ is a complemented set, and if $B, C$ are elements of $M$
such that $B < A < C$ and $\mu(B) = \mu(C)$, then $A \in M$.

As there is no indication of indexing in the description of $M$, the Bishop-Cheng definition of
a measure space seems to employ the powerset axiom in the formulation of $M$. The powerset axiom is
clearly used in $(\BMS_1)$ and $\BCM_3$.

The following definition of Bishop is given in [9], p. 183.

Bishop definition of a measure space. Let $F$ be a nonvoid family of real-valued functions on a
set $X$, such that $\epsilon - f \in F$ whenever $\epsilon > 0$ and $f \in F$. Let $\C F$ be any
family of complemented subsets of $X$ $($relative to $F)$, closed with respect
to countable unions, countable intersections, and complementation.
Let $\C M$ be a subfamily of $\C F$ closed under finite unions, intersections,
and differences. Let the function $\mu : \C M \to \Real^{0+}$ satisfy the following

$(\BMS_1)$ There exists a sequence $S_1 \subset S_2 \subset \ldots $ of elements of $\C M$ such
that[Bishop here means $\bigcup_{n = 1}^{\infty} S_n = X$.] $\bigcup_{n = 1}^{\infty} S_n = X_0$
and $\lim_{n \to \infty} \mu(A \cap S_n) = \mu (A)$ for all $A$ in $\C M$.

$(\BMS_2)$ If $A \in \C F$, and if there exist $B$ and $N$ in $\C M$ such that $(i)$ $\mu(N) = 0$,
$(ii)$ $x \in A$ whenever $x \in B - N$, and $(iii)$ $x \in -A$ whenever $x \in -B - N$, then $A \in \C M$
and $\mu(A) = \mu(B)$.

$(\BMS_3)$ If $A \in \C M$, if $B \in \C F$, and if $A \cap B \in \C M$, then $A - B \in \C M$ and
$\mu(A) = \mu(A - B) + \mu(A \cap B)$.

$(\BMS_4)$ We have $\mu(A) + \mu(B) = \mu(A \cup B) + \mu(A \cap B)$ for all $A$ and $B$ in $\C M$.

$(\BMS_5)$ For each sequence $\{An\}$ of sets in $\C M$ such that $c := \lim_{n \to \infty}
\mu\big(\bigcup_{k = 1}^n A_k\big)$ $[$respectively, $c := \lim_{n \to \infty} \mu\big(\bigcap_{k = 1}^n A_k\big)]$
exists, the set $A := \bigcup_{k = 1}^{\infty}A_k$ $($respectively, $A := \bigcap_{k = 1}^{\infty}A_k)$
is in $\C M$, and $\mu(A) = c$.

$(\BMS_6)$ Each $A$ in $\C M$ with $\mu(A) > 0$ is nonvoid.

Then the quintuple $(X, F, \C F, \C M, \mu)$ is called a measure space, $\mu$ is the
measure, $\C F$ is the class of Borel sets, and $\C M$ is the class of integrable sets.

If in Bishop's definition we understand the families of complemented subsets $\C F$ and $\C M$
as indexed families $(\B A)_{i \in I}, (\B A)_{j \in J}$ over some sets $I$ and $J$, respectively, with
$J \subseteq I$, then the quantifications involved in the clauses of Bishop's definition are over $I$ and $J$,
and not over some class. Since in [9], p. 65, a family of subsets of $X$ is defined as an
appropriate set-indexed family of sets, Bishop's first definition of measure space is predicative.

Regarding the exact definition of a measure space within the formal system $\Sigma$ introduced by Bishop
in [12],
Bishop writes in [12], p. 67, the following:

To formalize in $\Sigma$ the notion of an abstract measure space, definition 1 of chapter 7
of [9] must be
rewritten as follows. A measure space is a family $\C M \equiv \{A_t\}_{t \in T}$ of
complemented subsets
of a set $X$ relative to a certain family $\C F$ of real-valued function on $X$, a map $\mu : T \to \Real^{0+}$,
and an additional structure as follows: The void set $\emptyset$ is an element $A_{t_0}$ of $\C M$, and
$\mu(t_0) = 0$.
If $s$ and $t$ are in $T$, there exists an element $s \mathsmaller{\vee} t$ of $T$ such that
$A_{s \mathsmaller{\vee} t} < A_s \cup A_t$.
there exist operations $\mathsmaller{\wedge}$ and $\mathsmaller{\sim}$ on $T$, corresponding
to the set theoretic operations $\cap$ and $-$.
The usual algebraic axioms are assumed, such as $\mathsmaller{\sim}(s \ \mathsmaller{\vee} \ t) =
\mathsmaller{\sim} s \ \mathsmaller{\wedge} \ \mathsmaller{\sim} t$. Certain measure-theoretic
axioms, such as $\mu(s \ \mathsmaller{\vee} \ t) + \mu(s \ \mathsmaller{\wedge} \ t) = \mu(s) + \mu(t)$,
are also assumed. Finally, there exist operations $\vee$ and $\wedge$. If, for example, $\{t_n\}$
is a sequence such that $C \equiv \lim_{k \to \infty} \mu(t_1 \ \mathsmaller{\vee} \ldots
\mathsmaller{\vee} \ t_k)$
exists, then $\vee \{t_n\}$ is an element of $T$ with measure $C$. Certain axioms for $\vee$ and $\wedge$
are assumed. If $T$ is the family of measurable sets of a compact space relative to a measure $\mu$, and the
set-theoretic function $\mu : T \to \Real^{0+}$ and the associated operations are defined as indicated above,
the result is a measure space in the sense just described.

Considerations such as the above indicate that essentially all of the material in [9],
appropriately modified, can be comfortably formalised in $\Sigma$.

The expression $A_{s \mathsmaller{\vee} t} < A_s \cup A_t$ is probably a typo (it is the
writing $A_{s \mathsmaller{\vee} t} = A_s \cup A_t$, which expresses the “weak belongs to”
relation for $\lambda_0 I$). Bishop does not mention that $\C M$ is a set of complemented subsets of $X$,
he only says that it is a family of such sets. This is not the case in [19], p. 282. This explanation
given by Bishop regarding the explicit and unfolded writing of many of the definitions in constructive mathematics
refer to [9]. I have found no similar comment of Bishop with respect to his later measure theory,
developed with Cheng. Moreover, I have found no such comment in the extensive work of Chan on Bishop-Cheng
measure and probability theory.

In [80], p. 354, Myhill criticised Bishop for using a set of subsets $M$ in the definition of
a measure space, hence, according to Myhill, Bishop used the powerset axiom. Since $M$ is an $I$-set of
subsets of $X$, in the sense described in section <ref>, Myhill's critique is not
correct. Bishop's exaplanation in the previous extract is also a clear reply to a critique like Myhill's.
Notice that Myhill's paper [80] refers only to [9], and it does not mention [12],
which includes Bishop's clear explanation. This is quite surprising, as Myhill's paper, received in
January 1974, was surely written after the publication of [66], in which Bishop's paper [12] is included
and Myhill is one of its three editors!
Myhill's critique would be correct, if he was referring to the Bishop-Cheng measure space defined
in [18], a work published quite some time before Myhill submit [80]. Myhill though,
does not refer to [18] in [80].

Definition <ref> is the explicit writing within $\BST$ of the corresponding
definition in [19], pp. 216–217.

The following definition is given in [18], p. 2, and it is repeated in [19], p. 217.

Bishop-Cheng definition of an integration space.
A triplet $(X, L, I)$ is an integration space if $X$ is a nonvoid set with an inequality $\neq$, $L$
is a subset of $\C F(X)$ (this set is $\C F^{se}(X)$ in our terminology), and $I$ is a mapping of $L$
into $\Real$ such that the following properties holdBishop-Cheng definition of an integration space.

$(\BCIS_1)$ If $f, g \in L$ and $\alpha, \beta \in \Real$, then $\alpha f + \beta g $, $|f|$, and $f
\wedge 1$ belong to $L$, and $I(\alpha f + \beta g) = \alpha I(f) + \beta I(g)$.

$(\BCIS_2)$ If $f \in L$ and $(f_n)$ is a sequence of nonnegative functions in $L$ such that $\sum_{n}I(f_n)$
converges and $\sum_nI(f_n) < I(f)$, then there exists $x \in X$ such that $\sum_nf_n(x)$ converges
and $\sum_nf_n(x) < f(x)$.

$(\BCIS_3)$ There exists a function $p$ in $L$ with $I(p) = 1$.

$(\BCIS_4)$ For each $f$ in $L$, $\lim_{n \to \infty} I(f \wedge n) = I(f)$ and $\lim_{n \to \infty} I(|f| \wedge n^{-1}) = 0$.

The notion of an integration space is a constructive version of the Daniell integral,
introduced in [43]. The Bishop-Cheng definition of an integration space is impredicative, as
the class $\C F(X)$ is treated as a set. The notion of a subset is defined only for sets, and $L$ is
considered a subset of $\C F(X)$. The extensional character of $L$ is also not addressed. This
impredicative approach to $L$ is behind the simplicity of the Bishop-Cheng definition. E.g., in $(\BCIS_4)$
the formulation of the limit is immediate as the terms $f \wedge n \in L$ and $I$ is defined on $L$. In
Definition <ref> though, we need to use an element $\alpha(n)$ of the index-set $I$ such
that $f \wedge n =_{\C F(X)} f_{\alpha(n)}$, in order to express the limit.

The Bishop-Cheng definition of the “set” $L^1$$L^1$ (or $L^p$, $L^p$where $p \geq 1$)
of integrable functionsintegrable function is also impredicative, as it rests on
the use of the totality $\C F^{se}(X)$ as a set (see Definition (2.1) in [19], p. 222).
In [132], pp. 49–60, the pre-integration space $L^1$ of canonically integrable functions
is studied instead within $\BST$, as the completion of an integration space. The set $L^1$ is
predicatively defined in [9], p. 190, as an integrable function is an appropriate measurable
function, which is defined using quantification over the set-indexed family $\C M$ of integrable sets
in a Bishop measure space (see Note <ref>).

CHAPTER: EPILOGUE

§ $\BST$ BETWEEN DEPENDENT TYPE THEORY AND CATEGORY THEORY

Here we tried to show how the elaboration of the notion of a set-indexed family of
sets within $\BST$ expands the range of $\BISH$ both in its foundation and its practice.
Chapters <ref>-<ref> are concerned with the foundations of
$\BISH$, and chapters <ref> and <ref> with the practice of $\BISH$.

Chapter <ref> presents the set-like objects, the families of which are studied later:
sets, subsets, partial functions, and complemented subsets. Operations between these objects generate
corresponding operations between their families and family-maps. Chapter <ref>
includes the fundamental notions and results about set-indexed families of sets. A family of
sets $\Lambda \in \Fam(I)$, together with its $\sum$- and $\prod$-set, and a family map $\Psi \colon \Lambda \To M$,
are examples of notions with a strong type-theoretic, or categorical flavour, depending on the point of
observation view. This is not accident, as $\MLTT$ was motivated by Bishop's book [9].
Moreover, $\BST$ can roughly be described as a fundamental informal theory of totalities and assignment
routines, and (informal) category theory as a fundamental  (informal) theory of objects and arrows. A
fundamental similarity between $\BST$ and $\MLTT$ is the explicit use of dependency, which is suppressed in category theory. The fundamental categorical concepts of a functor and a natural transformation,
which are translated within $\BST$ as an $I$-family of sets and a family-map between $I$-families of sets,
have an immediate and explicit formulation within dependent type theory or within $\BST$
(see Note <ref>). The formulation of dependency though, within category theory is much
more involved (see e.g., [85]). On the other hand, a fundamental similarity between $\BST$ and
category theory is the use of definitions that do not “force”  facts and results, as in the case of
$\MLTT$ and its recent extension $\HoTT$. While the language of $\MLTT$ is clearly closer to $\BST$, a
large part of pure category theory, the size of the totalities involved excluded, follows the “pattern”
of doing constructive mathematics in the style of $\BISH$:  all notions are defined, no powerful axioms
are used, and despite the generality in the categorical formulations, most results have a concrete
algorithmic[The question of the constructive character of general category theory is addressed in [75].
There constructivism in mathematics is identified with Brouwer's intuitionism. The inclusion of Bishop-style constructivism
and of type-theoretic constructivism in the interpretation of mathematical constructivism is necessary and sheds more
light on the original question.] meaning.

The interconnections between category theory and dependent type theory is a standard theme behind
foundational studies on mathematics and theoretical computer science the last forty years. The recent explosion of univalent foundations, spearheaded
by the Fields medalist Vladimir Voevodsky, regenerated the study of these interconnections. The appropriate categorical understanding of the univalence axiom brought category-theorists and type-theorists even closer. $\BST$ seems to be
in some kind of common territory between dependent type theory and category theory. It also features
simultaneously the proof-irrelevance of category theory and classical mathematics,  and the proof-relevance of
$\MLTT$. In contrast to $\HoTT$, where a type $A$ has a rich space-structure due to the induction principle
corresponding to the introduction of the identity family $=_A \colon A \to A \to \C U$ on $A$, the notion
of space in $\BISH$, as in classical set-based mathematics, is not identical to that of a set. This is also
captured in category theory, where the category of sets behaves differently from the category of topological spaces.
We need to add, by definition, extra structure to a set $X$, in order to acquire a non-trivial space structure.
In this work the concept of space considered was that of a Bishop space. This is one option, which is shown to
be very fruitful, if we work within $\BISH^*$, but it is not the only one.

As in the case of $\MLTT$ or $\HoTT$, a non-trivial part of category theory can be studied within $\BST$. We gave a glimpse of that in Note <ref>. Working in a similar fashion, most of the theory of small categories can
appropriately be translated into $\BST$. This modelling of pure category theory “suffers”, as any modelling,
from the inclusion of features, like conditions $(\Cat_3), (\Cat_4)$, and $(\Funct_3)$, that depend on the
system $\BST$ itself and are not part of the original theory. In any event, such a translation is not meant
to be an attempt to replace pure category theory, but to embed into $\BISH$ concepts and facts from category
theory useful to the practice of $\BISH$. For example, all categorical notions and facts of constructive algebra
presented in [76], within a category theory irrelevant to the version of Bishop's theory of sets
underlying [76], can, in principle, be approached within $\BST$ and the corresponding category
theory within $\BST$.
Unfolding proof-relevance in $\BISH$ through $\BST$, categorical facts, like the Yoneda lemma
for $\Fam(\widehat{I})$

can be translated from $\MLTT + \FunExt$ to $\BISH$.
It remains to find though, interesting applications of such results to $\BISH$.

Inductive definitions bring the language of $\BISH^*$ closer to dependent type theory. The induction
principles that accommodate inductive definitions in the latter correspond to universal properties
in category theory. The formalisation of $\BST$, and its possible extension $\BST^*$ with inductive
definitions with rules of countably many premises, is an important open problem. The natural requirement
for a faithful and adequate formal system for $\BST$ and $\BST^*$ makes the choice of the formal framework
even more difficult. It seems that a version of a formal version of extensional Martin-Löf type theory,
and the corresponding theory of setoids within it, is a formal system very close to the informal system $\BST$.
As we have explained in Note <ref>, a formal version of intensional $\MLTT$ does
not seem to be a faithful formal system for the informal theory $\BISH$. The logical framework of an extensional version of dependent type theory though, and the identification of propositions with types, is quite far from the usual practice of $\BISH$, which is, in this respect, close to the standard practice of  classical mathematics. It is natural to search for a formal
system of $\BST$ where logic is not built in, as in $\MLTT$, and which reflects the way sets are defined in $\BST$.
We hope that the presentation of $\BST$ in this work will be helpful to the construction of such a formal counterpart.

Category theory can also be very helpful to the formulation of the properties of Bishop sets and functions.
The work of Palmgren [83] on the categorical properties of the category of setoids and setoid maps
within intensional $\MLTT$ is expected to be very useful to this. A similar formulation of the categorical
properties of the theory of setoids and setoid maps within extensional $\MLTT$ could be even closer to
the formulation of the categorical properties of Bishop sets and functions.

§ FURTHER OPEN QUESTIONS AND FUTURE TASKS

We collect here some further open questions and future tasks stemming form this work.

* To develop the theory of neighbourhood spaces using the notion of a neighbourhood family of
subsets of  a set $X$ that covers $X$ (see Note <ref>).

* Is it possible to use families of complemented subsets to describe a neighbourhood space? The
starting idea is to assign to each $i \in I$ a complemented subset $\B \nu_0(i) := \big(\nu_0^1(i),
\nu_0^0(i)\big)$ of $X$, such that $\nu_0^1(i)$ is open and
$\nu_0^0(i)$ is closed. The benefit of such an approach to constructive topology is that the classical
duality between open and closed sets is captured constructively.  E.g., the $1$-component of the
complement $- \B \nu_0(i) := \big(\nu_0^0(i), \nu_0^1(i)\big)$ of $\B \nu_0(i)$ is a closed set and
its $0$-component is an open set.

* Can we use complemented subsets of $\Nat$ in a constructive reconstruction of recursion theory,
instead of just subsets of $\Nat$? This question is inspired from the work of Nemoto on recursion theory
within intuitionistic logic.

* To explore further the notion of an impredicative set, and the hierarchy mentioned in
Note <ref>.

* To find interesting purely mathematical applications of set-relevant families of sets and
of families of families of sets.

* To investigate the possibility of a $\BHK$-interpretation of a negated formula
(see Note <ref>).

* To develop a (predicative) theory of ordinals within $\BST$.

* To study families of sets with a proof-relevant equality over an index-set with a proof-relevant equality.

* To translate more notions and results from $\MLTT$ and $\HoTT$ to $\BISH$ through $\BST$. As a special case,
to translate higher inductive types (HITs) into $\BISH$, other than the truncation $||A||$ of $A$. If we work
directly with a space in $\BST$ i.e., with a Bishop space $\C F := (X, F)$, and not with an arbitrary type,
as in $\HoTT$, we can define within $\BST$ notions like the conecone of a Bishop space and the
suspensionsuspension of a Bishop space of $\C F$.
If $\oi := [0, 1]$, we call $\D I_{\mathsmaller{01}}^{\mcup} := \{0\} \cup (0, 1) \cup \{1\}$ the
pseudo-interval $[0, 1]$pseudo-interval $[0, 1]$. To $\D I_{\mathsmaller{01}}^{\mcup}$
we can associate the least Bishop topology generated by the restriction of the identity map to it. The
relation $\sim_X^{\tau}$ on $X \times \oic$, defined by

\[ (x, i) \eqt (x{'}, i{'})  : \TOT \big( i, i{'} \in \{0\} \cup (0, 1) \ \& \ i =_{\oic} i{'} \ \& \ x =_X x{'} \big)
\ \  \mbox{or} \ \   i =_{\oic} 1 =_{\oic} i{'},\]

is an extensional equivalence relation. If $Y := X \times \oic$ and $\tau_0^X \colon Y \to \tau_0^X Y$ is the function that maps $(x, i)$ to its equivalence class (see section <ref>), then $\tau_0^X Y(Y)$, equipped with an an appropriate Bishop topology, is the conecone of a Bishop space of $\C F$. For the suspension of $\C F$ wesuspension of a Bishop space work similarly.

* To find interesting mathematical applications of $(-2), (-1)$- and $0$-sets in $\BISH$.

* To elaborate the study of category theory within $\BST$. So far we have formulated within $\BST$ most of the category theory formulated within the Calculus of Inductive Constructions in [61].

* To develop along the lines of Chapter <ref> the theory of spectra of other structures,
like groups, rings, modules etc.

* To develop further the theory of Borel sets of a Bishop topology. E.g., to find the exact
relation between the Borel sets $\Borel(\C F)$ and $\Borel(\C G)$ and the Borel sets $\Borel(\C F \times \C G)$
of the product Bishop space $\C F \times \C G$. And similarly for all important constructions of new Bishop
spaces from given ones.

* To formulate various parts of the constructive algebra developed in [76] and [68] within $\BST$.

* To elaborate the theory of (pre-)measure spaces and (pre-)integrations spaces. The past work [132]
and the forthcoming work [104] are in this direction.

* To approach Chan's probability theory in [35], which is within $\BCMT$,
through a predicative reconstruction of $\BCMT$ within $\BST$.

CHAPTER: APPENDIX

§ BISHOP SPACES

We present the basic notions and facts on Bishop spaces that are used in the previous sections.
For all concepts and results from constructive real analysis that we use here without
further explanation we refer to [19]. For all proofs that are not included in this section we
refer to [88]. We work within the extension $\BISH^*$ of $\BISH$ with inductive definitions
with rules of countably many premises. A Bishop space is a constructive, function-theoretic
alternative to the classical notion of a topological space, and a Bishop morphism is the
corresponding function-theoretic notion of “continuous function” between Bishop spaces.

If $X$ is a set and $\Real$ is the set of real numbers, we denote by $\mathbb{F}(X)$
the set of functions from $X$ to $\Real$, and by $\Const(X)$$\Const(X)$ the
subset of $\mathbb{F}(X)$ of all constant functions on $X$.
If $a \in \Real$, we denote by $\overline{a}^X$$\overline{a}^X$
the constant function on $X$ with value $a$. We denote by $\Nat^+$ the set of non-zero natural numbers.
A function $\phi: \Real \rightarrow \Real$ is called Bishop continuous, or simply continuous,
if for every $n \in \Nat^+$ there is a function$\omega_{\phi,n}$ $\omega_{\phi, n}:
\mathbb{R}^{+} \rightarrow \mathbb{R}^{+}$,
$\epsilon \mapsto \omega_{\phi, n}(\epsilon)$, which is called a modulus
of continuitymodulus of (uniform) continuity of $\phi$ on $[-n, n]$, such that the following
condition is satisfied

\[\forall_{x, y \in [-n, n]}(|x - y| < \omega_{\phi, n}(\epsilon) \Rightarrow
|\phi(x) - \phi(y)| \leq \epsilon),\]

for every $\epsilon > 0$ and every $n \in \Nat^+$. We denote by $\BR$$\BR$ the set of continuous functions
from $\Real$ to $\Real$, which is equipped with the equality inherited from $\D F(\Real)$.

Note that we could have defined the modulus of continuity $\omega_{\phi, n}$ as a function from $\Nat^+$
to $\Nat^+$. Clearly, a continuous function $\phi \colon \Real \to \Real$ is uniformly continuous on every bounded
subset of $\Real$. The latter is an impredicative formulation of uniform continuity, since it
requires quantification over the class of all subsets of $\Real$. The formulation of uniform continuity
in the Definition <ref> though, is predicative, since it requires quantification over the sets
$\Nat^+, \D F(\Real^+, \Real^+)$ and $[-n, n]$.

If $X$ is a set, $f, g \in \mathbb{F}(X)$, $\epsilon > 0$, and $\Phi \subseteq \mathbb{F}(X)$,
let$U(X; \Phi, g, \epsilon)$

\[ U(X; f, g, \epsilon) :\TOT \forall_{x \in X}\big(|g(x) - f(x)| \leq \epsilon\big),\]

\[ U(X; \Phi, f) :\TOT \forall_{\epsilon > 0}\exists_{g \in \Phi}\big(U(f, g, \epsilon)\big).\]

If the set $X$ is clear from the context, we write simpler $U(f, g, \epsilon)$$U(f,g, \epsilon)$
and$U(\Phi, f)$ $U(\Phi, f)$, respectively.$U(X; \Phi, f)$
We denote by $\Phi^*$ the bounded elements of $\Phi$, and its uniform
closureuniform closure $\overline{\Phi}$ is defined by$\overline{\Phi}$

\[ \overline{\Phi} := \{f \in \D F(X) \mid U(\Phi, f)\}.\]

A Bishop topology on $X$ is a certain subset of $\D F(X)$. Since the Bishop topologies considered here
are all extensional subsets of $\D F(X)$, we do not mention the embedding $i_F^{\D F(X)} \colon F \eto \D F(X)$,
which is given in all cases by the identity map-rule.

A Bishop spaceBishop space is a pair $\C F := (X, F)$, where $F$ is an extensional subset of $\D F(X)$,
which is called a Bishop topology, or simply a topologyBishop topology
of functions on $X$, that satisfies the following conditions:

$(\BS_1)$ If $a \in \Real$, then $\overline{a}^X \in F$.

$(\BS_2)$ If $f, g \in F$, then $f + g \in F$.

$(\BS_3)$ If $f \in F$ and $\phi \in \Bic(\Real)$, then $\phi \circ f \in F$

(E) at (0,0) $X$;
[right=of E] (F) $\Real$;
[below=of F] (A) $\Real$.;

[->] (E)–(F) node [midway,above] $f$;
[->] (E)–(A) node [midway,left] $F \ni \phi \circ f \ $;
[->] (F)–(A) node [midway,right] $\phi \in \BR$;

$(\BS_4)$ $\overline{F} = F$.

If $\C F := (X, F)$ is a Bishop space, then $\C F^* := (X, F^*)$ is the Bishop space of
bounded$\C F^*$$F^*$ elements of $F$. The constant functions
$\Const(X)$ is the trivial
topology on $X$, while $\D F(X)$ is the discrete topology on $X$. Clearly, if $F$ is a topology on $X$,
then $\Const(X) \subseteq F \subseteq \D F(X)$, and the set of its bounded elements
$F^{*}$ is also a topology on $X$. It is straightforward to see that the pair $\C R := (\Real, \BR)$ is a
Bishop space, which we call the Bishop space of reals.
A Bishop topology $F$ is a ring and a lattice; since $|\id_{\Real}| \in \Bic(\Real)$, where $\id_{\Real}$ is the
identity function on $\Real$, by BS$_{3}$ we get that if $f \in F$ then $|f| \in F$.
By BS$_{2}$ and BS$_{3}$, and using the following equalities

\[ f{\cdot}g = \frac{(f + g)^{2} - f^{2} - g^{2}}{2} \in F,\]

\[ f \vee g = \max\{f, g\} = \frac{f + g + |f - g|}{2} \in F, \]

\[ f \wedge g = \min\{f, g\} = \frac{f + g - |f - g|}{2} \in F,\]

we get similarly that if $f, g \in F$, then $f{\cdot}g, f \vee g, f \wedge g \in F$.

Turning the definitional clauses of a Bishop topology into inductive rules, Bishop defined in [9], p. 72,
the least topology including a given subbase $F_{0}$. This inductive definition, which
is also found in [19], p. 78, is crucial to the definition of new Bishop topologies from given ones.

The Bishop closure of $F_{0}$, or the least topologyleast Bishop topology
$\bigvee{F_{0}}$$\bigvee F_0$
generated by some $F_{0} \subseteq \mathbb{F}(X)$, is defined by the following inductive rules:

\[ \frac{f_{0} \in F_{0}}{f_{0} \in \bigvee F_{0}}, \ \ \ \frac{a \in \Real}{\overline{a}^{X} \in
\bigvee F_{0}},
\ \ \ \frac{f, g \in \bigvee F_{0}}{f + g \in \bigvee F_{0}}, \ \ \  \frac{f \in \bigvee F_{0}, \
g =_{\D F(X)} f}{g \in \bigvee F_{0}},\]

\[ \frac{f \in \bigvee F_{0}, \ \phi \in \Bic(\Real)}{\phi \circ f \in \bigvee F_{0}},
\ \ \ \ \ \frac{\big(g \in \bigvee F_{0}, \ U(f, g, \epsilon)\big)_{\epsilon > 0}}{f \in \bigvee F_{0}}.\]

We call $\bigvee F_{0}$ the Bishop closure of $F_{0}$, and $F_{0}$ a subbasesubbase of
$\bigvee F_{0}$.

If $F_{0}$ is inhabited, then $(\BS_1)$ is provable by $(\BS_3)$. The last, most complex rule
above can be replaced by the rule

\[ \frac{g_{1} \in \bigvee F_{0} \ \wedge \ U\big(f, g_{1}, \frac{1}{2}\big),
\ \  g_{2} \in \bigvee F_{0} \ \wedge \
U\big(f, g_{2}, \frac{1}{2^{2}}\big), \   \ldots}{f \in \bigvee F_{0}},\]

a rule with countably many premisses.
The corresponding induction principle $\Ind_{\bigvee F_{0}}$$\Ind_{\bigvee F_0}$ is

\[\bigg[\forall_{f_{0} \in F_{0}}\big(P(f_{0})\big) \ \& \
\forall_{a \in \mathbb{R}}\big(P(\overline{a}^{X})\big) \
\&  \ \forall_{f, g \in \bigvee F_{0}}\big(P(f) \ \& \ P(g) \Rightarrow P(f + g) \]

\[ \& \ \forall_{f \in \bigvee F_0}\forall_{g \in \D F(X)}\big(g =_{\D F(X)} f \To P(g)\big)\]

\[ \& \ \forall_{f \in \bigvee F_{0}}\forall_{\phi \in \Bic(\mathbb{R})}\big(P(f)
\Rightarrow P(\phi \circ f)\big) \]

\[\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \& \  \forall_{f \in \bigvee F_{0}}\big(
\forall_{\epsilon > 0}\exists_{g \in \bigvee F_{0}}(P(g) \ \& \ U(f, g, \epsilon))
\Rightarrow P(f)\big)\bigg]\]

\[\Rightarrow \forall_{f \in \bigvee F_{0}}\big(P(f)\big),\]

where $P$ is any bounded formula.
Next we define the notion of a Bishop morphismBishop morphism between Bishop spaces.
The Bishop morphisms are the arrows in the category of Bishop$\Bis$ spaces $\Bis$.

If $\C F := (X, F)$ and $\C G = (Y, G)$ are Bishop spaces, a function $h: X \rightarrow Y$ is called
a Bishop morphism, if $\forall_{g \in G}(g \circ h \in F)$

(E) at (0,0) $X$;
[right=of E] (F) $Y$;
[below=of F] (A) $\Real$.;

[->] (E)–(F) node [midway,above] $h$;
[->] (E)–(A) node [midway,left] $F \ni g \circ h \ $;
[->] (F)–(A) node [midway,right] $g \in G$;

We denote by $\Mor(\C F, \C G)$$\Mor(\C F, \C G)$ the set of Bishop morphisms
from $\C F$ to $\C G$. As $F$ is an extensional subset of $\D F(X)$, $\Mor(\C F, \C G)$ is an
extensional subset of $\D F(X,Y)$.  If $h \in \Mor(\C F, \C G)$, the induced mapping
$h^* \colon G \to F$ from $h$induced mapping from a Bishop morphism$h^*$
is defined by the rule

\[ h^*(g) := g \circ h; \ \ \ \ g \in G.\]

If $\mathcal{F} := (X, F)$ is a Bishop space, then $F = \Mor(\mathcal{F}, \mathcal{R})$,
and one can show inductively that if $\C G := (Y, \bigvee G_0)$, then
$h: X \rightarrow Y \in \Mor(\mathcal{F}, \C G)$ if and only if
$\forall_{g_{0} \in G_{0}}(g_{0} \circ h \in F)$

(E) at (0,0) $X$;
[right=of E] (F) $Y$;
[below=of F] (A) $\Real$.;

[->] (E)–(F) node [midway,above] $h$;
[->] (E)–(A) node [midway,left] $F \ni g_0 \circ h \ \ $;
[->] (F)–(A) node [midway,right] $g_0 \in G_0$;

We call this fundamental fact the$\bigvee$-lifting of morphisms $\bigvee$-lifting of morphisms.
A Bishop morphism is a Bishop isomorphismBishop isomorphism, if it is an isomorphism in
the category $\Bis$. We write $\C F \simeq \C G$$\C F \simeq \C G$ to denote that $\C F$ and $\C G$
are Bishop isomorphic. If $h \in \Mor(\C F, \C G)$ is a bijection, then
$h$ is a Bishop isomorphism if and only if it is openopen morphism i.e.,
$\forall_{f \in F}\exists_{g \in G}\big(f = g \circ h\big)$.

Let $\C F := (X, F), \C G := (Y, G)$ be Bishop spaces, and $(A, i_A) \subseteq X$

The product Bishop spaceproduct Bishop space
$\C F \times \C G := (X \times Y, F \times G)$ of $\C F$$F \times G$
and $\C G$, the relativerelative Bishop space Bishop space $\Fii_{|A} := (A, F_{|A})$ on $A$, and
the pointwise exponential Bishop space$F_{|A}$ $F \to G$
$\mathcal{F} \rightarrow \mathcal{G} = (\Mor(\mathcal{F}, \mathcal{G}),
F \rightarrow G)$ are defined, respectively, by

\[ F \times G := \bigvee \left[\{f \circ \pr_{X}, \mid f \in F\} \cup \{g \circ \pr_{Y} \mid g \in G\}\right]
=: \bigvee_{f \in F}^{g \in G}f \circ \pr_{X}, g \circ \pr_{Y},\]

\[ F_{|A} = \bigvee \{f_{|A} \mid f \in F\} =: \bigvee_{f \in F}f_{|A}\]

(E) at (0,0) $A$;
[right=of E] (F) $X$;
[right=of F] (B) $\Real$,;

[right hook->] (E)–(F) node [midway,above] $i_A$;
[->] (F)–(B) node [midway,above] $f$;
[->,bend right] (E) to node [midway,below] $f_{|A}$ (B);

\[ F \rightarrow G := \bigvee \big\{\phi_{x, g} \mid x \in X, g \in G \big\} :=
\bigvee_{x \in X}^{g \in G}\phi_{x, g},\]

\[ \phi_{x, g}: \Mor(\mathcal{F}, \mathcal{G}) \rightarrow \mathbb{R}, \ \ \ \ \phi_{x, g}(h) = g(h(x));
\ \ \ \ x \in X, \ g \in G.\]

One can show inductively the following $\bigvee$-liftings

\begin{align*}
\bigvee F_{0} \times \bigvee G_{0} & := \bigvee \left[\{f_{0} \circ \pr_{X}, \mid f_{0} \in F_{0}\} \cup
\{g_{0} \circ \pr_{Y} \mid g_{0} \in G_{0}\}\right]\\
& =: \bigvee_{f_{0} \in F_{0}}^{g_{0} \in G_{0}}f_{0} \circ \pr_{X}, g_{0} \circ \pr_{Y},
\end{align*}

\[ \big(\bigvee F_{0}\big)_{|A} = \bigvee \{{f_{0}}_{|A} \mid f_{0} \in F_{0}\} =: \bigvee_{f_{0}
\in F_{0}}{f_{0}}_{|A},\]

\[ F \rightarrow \bigvee G_0 = \bigvee \big\{\phi_{x, g_0} \mid x \in X, g_0 \in G_0 \big\} :=
\bigvee_{x \in X}^{g_0 \in G_0}\phi_{x, g_0}.\]

The relative topology $F_A$ is the least topology on $A$ that makes $i_A$ a Bishop morphism, and
the product topology $F \times G$ is the least topology on $X \times Y$
that makes the projections $\pr_X$ and $\pr_Y$ Bishop morphisms. The term pointwise exponential Bishop
topology is due to the fact that $F \to G$ behaves like the the classical topology of the pointwise convergence
on $C(X, Y)$, the set of continuous functions from the topological space $X$ to the topological space $Y$.

§ DIRECTED SETS

Let $I$ be a set and $i \lt_I j$ a binary extensional relationbinary extensional relation on $I$ i.e.,

\[\forall_{i, j, i{'}, j{'} \in I}\big(i =_I i{'} \ \& \ j =_I j{'} \ \& \ i \lt_I j \To i{'} \lt_I j{'}\big).\]

If $i \lt_I j$ is reflexive and transitive, then $(I, \lt_I)$ is called a
a preorderpreorder. We call a preorder $(I, \lt_I)$ a directed setdirected set, and
inverse-directedinverse-directed set, respectively, if

\[ \forall_{i, j \in I}\exists_{k \in I}\big(i \lt_I k \ \& \ j \lt_I k\big), \]

\[\forall_{i, j \in I}\exists_{k \in I}\big(i \mt_I k \ \& \ j \mt_I  k\big) .\]

The covariant covariant diagonalcovariant diagonal $D^{\lt}(I)$$D^{\lt}(I)$ of $\lt_I$, the
contravariant diagonalcontravariant diagonal $D^{\mt}(I)$$D^{\mt}(I)$ of $\lt_I$, and
the $\lt_I$-upper set $I_{ij}^{\lt}$$I_{ij}^{\lt}$
of $i, j \in I$$\lt_I$-upper set are defined, respectively, by

\[ D^{\lt}(I) := \big\{(i, j) \in I \times I \mid i \lt_I j \big\}, \]

\[ D^{\mt}(I) := \big\{(j, i) \in I \times I \mid j \mt_I i \big\}, \]

\[ I_{ij}^{\lt} := \{k \in I \mid  i \lt_I k \ \& \ j \lt_I k\}. \]

Since $i \lt_I j$ is extensional, $D^{\lt}(I), D^{\mt}(I)$, and $I_{ij}^{\lt}$ are extensional
subsets of $I \times I$.

Let $(I, \lt_I)$ be a poset i.e., a preorder such that $\big[i \lt_I j \ \& \ j \lt_I i \big]\To i =_I j$, for every
$i, j, \in I$. A modulus of directednessmodulus of directedness for $I$ is a
function $\delta \colon I \times I \to I$, such
that for every $i, j, k \in I$ the following conditions are satisfied:

$(\delta_1)$ $i \lt_I \delta(i, j)$ and $j \lt_I \delta(i, j)$.

$(\delta_2)$ If $i \lt_I j$, then $\delta(i, j) =_I \delta(j, i) =_I j$.

$(\delta_3)$ $\delta\big(\delta(i, j), k\big) =_I \delta\big(i, \delta(j, k)\big)$.

In what follows we avoid for simplicity the use of subscripts on the relation symbols.
If $(I, \lt)$ is a preordered set and $(J, e) \subseteq I$, where $e : J \hookrightarrow I$,
and using for simplicity the same symbol $\lt$, if we define
$j \lt j{'} : \TOT e(j) \lt e(j{'}),$
for every $j, j{'} \in J$, then $(J, \lt)$ is only a preordered set. If $J$ is a cofinal subset of $I$,
which classically it is defined by the condition
$\forall_{i \in I}\exists_{j \in J}\big(i \lt j \big)$, then $(J, \lt)$ becomes a
directed set. To avoid the use of dependent choice, we add in the definition of a cofinal subset $J$
of $I$ a modulus of cofinality for $J$.

Let $(I, \lt)$ be a directed set and $(J, e) \subseteq I$, and let
$j \lt j{'} : \TOT e(j) \lt e(j{'})$, for every $j, j{'} \in J$. We say that $J$ is
cofinal in $I$, if there is a function $\cof_J : I \to J$, which we call a modulus of
cofinality of $J$ in $I$, that satisfies the following conditions:

$(\Cf_1)$ $\forall_{j \in J}\big(\cof_J(e(j)) =_J j\big)$.

(E) at (0,0) $J$;
[right=of E] (F) $I$;
[right=of F] (A) $J$.;

[right hook->] (E)–(F) node [midway,below] $e$;
[->] (F)–(A) node [midway,below] $\cof_J$;

[->,bend left] (E) to node [midway,above] $\id_J$ (A) ;

$(\Cf_2)$  $\forall_{i, i{'} \in I}\big(i \lt i{'} \To \cof_J(i) \lt \cof_J(i{'})\big)$.

$(\Cf_3)$ $\forall_{i \in I}\big(i \lt e(\cof_J (i))\big)$.

We denote the fact that $J$ is cofinal in $I$ by $(J, e, \cof_J) \subseteq^{\cof} I$, or, simpler, by$(J, e, \cof_J)
\subseteq^{\cof} I$$J \subseteq^{\cof} I$$J \subseteq^{\cof} I$.

Taking into account the embedding $e$ of $J$ into $I$, the condition (iii) is the exact writing of
the classical defining condition $\forall_{i \in I}\exists_{j \in J}\big(i \lt j \big)$.
To add the condition (i) is harmless, since $\lt$ is reflexive. If we consider the condition (iii) on $e(j)$,
for some $j \in J$, then by the condition (i) we get the transitivity $e(j) \lt e(\cof_J (e(j)))  = e(j)$.
The condition (ii) is also harmless to add. In the classical setting if $i \lt i{'}$, and $j, j{'} \in J$
such that $i \lt j$ and $i{'} \lt j{'}$, then there is some $i{''} \in I$ such that $j{'} \lt i{''}$ and
$j \lt i{''}$. If $i{''} \lt j{''}$, for some $j{''} \in J$,

(E) at (0,0) $i$;
[above=of E] (F) ;
[right=of F] (A) $j$;
[left=of F] (B) $i{'}$;
[above=of B] (C) $j{'}$;
[above=of C] (D) ;
[right=of D] (H) $i{''}$;
[above=of H] (G) $j{''}$;

[->] (E)–(B) node [midway,below] ;
[->] (E)–(A) node [midway,left] ;
[->] (B)–(C) node [midway,below] ;
[->] (C)–(H) node [midway,right] ;
[->] (A)–(H) node [midway,right] ;
[->] (H)–(G) node [midway,right] ;

then $j \lt j{''}$. Since $i{'} \lt j{''}$ too,
the condition (ii) is justified. The added conditions (i) and (ii) are used in the proofs of
Theorem <ref> and Lemma <ref>(ii), respectively. Moreover, they are used
in the proof of Theorem <ref>.
The extensionality of $\lt$
is also used in the proofs of Theorem <ref> and Theorem <ref>.

E.g., if $\Even$ and $\Odd$ denote the sets of even and odd natural numbers, respectively,
let $e \colon \Even \eto \Nat$, defined by the identity map-rule, and $\cof_{\Even} \colon \Nat \to 2 \Nat$,
defined by the rule

\[ \cof_{2 \Nat}(n) := \left\{ \begin{array}{ll}
n    &\mbox{, $n \in \Even$}\\
n+1           &\mbox{, $n \in \Odd$.}
\end{array}
\right.\]

Then $(\Even, e, \cof_{\Even}) \subseteq \Nat$.

If $(I, \lt)$ is a directed set and $(J, e, \cof_J) \subseteq^{\cof} I$, then $(J, \lt)$ is directed.

Let $j, j{'} \in J$ and let $i \in I$ such that $e(j) \lt i$ and $e(j{'}) \lt i$. Since $i \lt e(\cof_J (i))$,
we get $e(j) \lt e(\cof_J (i))$ and $e(j{'}) \lt e(\cof_J (i))$ i.e., $j \lt \cof_J(i)$ and $j{'} \lt \cof_J(i)$.

[1] P. Aczel, M. Rathjen: Constructive Set Theory, book draft, 2010.
[2] S. Awodey: Axiom of Choice and Excluded Middle in Categorical Logic, Bulletin of Symbolic Logic,
volume 1, 1995, 344.
[3] S. Awodey: Category Theory, Oxford University Press, 2010.
[4] A. Bauer, A. Swan: Every metric space is separable in function realizability, arXiv:1804.

00427, 2018.
[5] M. J. Beeson: Formalizing constructive mathematics: why and how, in [107], 1981, 146–190.
[6] M. J. Beeson: Problematic principles in constructive mathematics, in D. van Dalen, D. Lascar,
J. Smiley (Eds.) Logic Colloquium '80, North-Holland, 1982, 11–55.
[7] M. J. Beeson: Foundations of Constructive Mathematics, Ergebnisse der
Mathematik und ihrer Grenzgebiete, Springer Verlag, 1985.
[8] S. Bhat, A. Agarwal, R. Vuduc: A type theory for probability density
functions, POPL'12, ACM, 2012, 545–556.
[9] E. Bishop: Foundations of Constructive Analysis, McGraw-Hill, 1967.
[10] E. Bishop: A General Language, unpublished manuscript, 1968(9)?
[11] E. Bishop: How to Compile Mathematics into Algol, unpublished manuscript, 1968(9)?
[12] E. Bishop: Mathematics as a Numerical Language, in [66], 1970, 53–71.
[13] E. Bishop: The Neat Category of Stratified Spaces, unpublished manuscript, University of
California, San Diego, 1971.
[14] E. Bishop: Aspects of Constructivism, Notes on the lectures delivered at the Tenth Holiday
Mathematics Symposium held at New Mexico State University, Las Cruses, during the period December 27-31, 1972.
[15] E. Bishop: Schizophrenia in Contemporary Mathematics, American Mathematical
Society Colloquium Lectures, Missoula University of Montana 1973, and in [110].
[16] E. Bishop: The crisis in contemporary mathematics, Historia Mathematics 2, 1975, 507–517.
[17] Selected Papers, Errett Bishop, edited by J. Wermer, World Scientific Publishing,
Singapore and Philadelphia, 1986.
[18] E. Bishop and H. Cheng: Constructive Measure Theory, Mem. Amer. Math. Soc. 116, 1972.
[19] E. Bishop and D. S. Bridges: Constructive Analysis, Grundlehren der math.
Wissenschaften 279, Springer-Verlag, Heidelberg-Berlin-New York, 1985.
[20] D. S. Bridges and F. Richman: Varieties of Constructive Mathematics,
Cambridge University Press, 1987.
[21] D. Bridges, O. Demuth: On the Lebesgue measurability of continuous functions in
constructive analysis, Bulletin of the American Mathematical Society, Vol. 24, No. 2, 1991, 259–276.
[22] D. S. Bridges and S. Reeves: Constructive Mathematics in Theory and Programming Practice,
Philosophia Mathematica (3), 1999, 65–104.
[23] D. S. Bridges: Constructive mathematics; a foundation for computable analysis,
Theoretical Computer Science 219, 1999, 95–109.
[24] D. S. Bridges and L. S. Vîţă: Techniques of Constructive Analysis,
in: Universitext, Springer, New York, 2006.
[25] 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.
[26] D. S. Bridges: Reflections on function spaces, Annals of Pure and Applied Logic 163, 2012, 101–110.
[27] G. Cantor: Über unendliche, lineare Punktmannichfaltigkeiten, Nummer 3. Mathematische
Annalen, 20, 1882, 113–121.
[28] D. S. Bridges, H. Ishihara, M. Rathjen, H. Schwichtenberg (Eds.): Handbook of Bishop Constructive
Mathematics, Cambridge University Press, to appear, 2021.
[29] C. Carathéodory: Mass und Integral und ihre algebraisierung, Springer Basel AG, 1956.
[30] Y. K. Chan: A constructive approach to the theory of stochastic processes, Transactions
of the American Mathematical Society, Vol. 65, 1972, 37–44.
[31] Y. K. Chan: A constructive study of measure theory, Pacific Journal of Mathematics, Vol. 41, No. 1,
1972, 63–79.
[32] Y. K. Chan: A constructive approach to the theory of stochastic processes,
Transactions of the American Mathematical Society, Vol. 165, 1972, 37–44.
[33] Y. K. Chan: Notes on constructive probability theory, The Annals of Probability, Vol. 2,
No. 1, 1974, 51–75.
[34] Y. K. Chan: A short proof of an existence theorem in constructive measure theory,
Proceedings of the American Mathematical Society, Vol. 48, No. 2, 1975, 435–436.
[35] Y. K. Chan: Foundations of Constructive Probability Theory, arXiv:1906.01803v2, 2019.
[36] R. L. Constable et al. Implementing Mathematics with the Nuprl Proof Development
373 System, Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1986.
[37] T. Coquand, H. Persson: Integrated Development of Algebra in Type Theory, preprint, 1998.
[38] T. Coquand, E. Palmgren: Metric Boolean algebras and constructive measure theory, Arch. Math. Logic
41, 2002, 687–704.
[39] T. Coquand, P. Dybjer, E. Palmgren, A. Setzer: Type-theoretic Foundations of
Constructive Mathematics, book-draft, 2005.
[40] T. Coquand, A. Spiwack: Towards Constructive Homological Algebra in Type Theory, in LNCS 4573,
2007, 40–54.
[41] T. Coquand, B. Spitters: Integrals and valuations, Journal of Logic $\&$ Analysis, 1:3, 2009, 1–22.
[42] T. Coquand: A remark on singleton types, manuscript, 2014, available at
http://www.cse.chalmers.se/$\sim$coquand/singl.pdf, 2014.
[43] P. J. Daniell: A general form of integral, Annals of mathematics, Second Series, 19 (4),
1918, 279–294.
[44] R. Dedekind: Was sind und was sollen die Zahlen?, 1. Auflage, Vieweg, Braunschweig, 1888.
[45] J. Dugundji: Topology, Allyn and Bacon, 1966.
[46] A. Edalat: A computable approach to measure and integration theory, Information and Computation
207, 2009, 642–659.
[47] F. Faissole, B. Spitters: Synthetic topology in Homotopy Type Theory for probabilistic
programming, preprint, 2016.
[48] S. Feferman: A language and axioms for explicit mathematics, in
J. N. Crossley (Ed.) Algebra and Logic, Springer Lecture Notes 450, 1975, 87–139.
[49] S. Feferman: Constructive theories of functions and classes, in Boffa et al. (Eds.)
Logic Colloquium 78, North-Holland, 1979, 159–224.
[50] H. Friedman: The consistency of classical set theory relative to a set theory with
intuitionistic logic, J. Symbolic Logic, 38, 1973, 315–319.
[51] H. Friedman: Set theoretic foundations for constructive analysis, Annals of Math. 105,
1977, 1–28.
[52] L. Gillman, M. Jerison: Rings of Continuous Functions, Van Nostrand, 1960.
[53] R. Godement: Topologie algébrique et théorie de faisceaux, Hermann, Paris, 1973.
[54] R. Goldblatt: Topoi, The Categorical Analysis of Logic, North-Holland, 1984.
[55] N. Greenleaf: Liberal constructive set theory, in [107], 1981, 213–240.
[56] N. D. Goodman, R. E. Vesley: Obituary: John R. Myhill (1923-1987), History and Philosophy of Logic,
8, 1987, 243–244.
[57] P. R. Halmos: Measure theory, Springer-Verlag New York Inc. 1974.
[58] F. Hausdorff: Grundzüge der Mengenlehre, Veit $\&$ Comp., Leipzig 1914
(reproduced in Srishti D. Chatterji et al. (Eds.): Felix Hausdorff. Gesammelte Werke. Band II:
Grundzüge der Mengenlehre, Springer, Berlin 2002).
[59] A. Heyting: Intuitionism, An introduction, North-Holland, 1956.
[60] E. Hewitt: Linear functionals on spaces of continuous functions, Fund. Math. 37, 1950, 161–189.
[61] G. Huet, A. Saïbi: Constructive Category Theory, in Proceedings of the joint CLICS-TYPES workshop on categories and type theory, Goteborg, MIT Press, 1998.
[62] H. Ishihara, E. Palmgren: Quotient topologies in constructive set theory and type theory, Annals of
Pure and Applied Logic 141, 2006, 257–265.
[63] H. Ishihara: Relating Bishop's function spaces to neighborhood spaces, Annals of Pure and
Applied Logic 164, 2013, 482–490.
[64] L. Jaun: Category Theory in Explicit Mathematics, PhD Thesis, University of Bern, 2019.
[65] P. T. Johnstone: Sketches of an Elefant A Topos Theory Compendium, Volume 1,
Oxford University Press, 2002.
[66] A. Kino, J. Myhill, R. E. Vesley (Eds.): Intuitionism and Proof Theory,
North-Holland, 1970.
[67] A. N. Kolmogoroff: Algèbres de Boole métrique complètes, VI Zjazd Mathematyków Polskich,
Warwaw, 1948, 21–30.
[68] H. Lombardi, C. Quitté: Commutative Algebra: Constructive Methods, Springer, 2015.
[69]  R. S. Lubarsky, M. Rathjen: On the regular extension axiom and its variants,
Mathematical Logic Quarterly 49 (5), 511–518, 2003.
[70] M. E. Maietti: A minimalist two-level foundation for constructive mathematics,
Annals of Pure and Applied Logic 160(3), 2009, 319–354.
[71] P. Martin-Löf: Notes on Constructive Mathematics, Almqvist and Wiksell, 1970.
[72] 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,North-Holland, 1975, 73–118.
[73] P. Martin-Löf: Intuitionistic type theory: Notes by Giovanni Sambin on a series
of lectures given in Padua, June 1980, Napoli: Bibliopolis, 1984.
[74] P. Martin-Löf: An intuitionistic theory of types, in [112], 127–172.
[75] C. McLarty: Two Constructicist Aspects of Category Theory, Philosophia Scienti$\oe$, Cahier spécial 6, 2006, 95–114.
[76] R. Mines, F. Richman, W. Ruitenburg: A course in constructive algebra, Springer
Science$+$Business Media New York, 1988.
[77] J. Myhill: Formal systems of intuitionistic analysis I, in van Rootselaar and Stall (Eds.)
Logic, methodology and philsosphy of science III, North-Holland, Amsterdam, 1968, 161–178.
[78] J. Myhill: Formal systems of intuitionistic analysis II, in [66], 1970, 151–162.
[79] J. Myhill: Some properties of intuitionistic Zermelo-Fraenkel set theory, in A. Matthias ,
H. Rogers (Eds.) Cambridge Summer School in Mathematical Logic, LNM 337, Springer, 1972, 206–231.
[80] J. Myhill: Constructive Set Theory, J. Symbolic Logic 40, 1975, 347-382.
[81] E. Palmgren: Bishop's set theory, Slides from TYPES Summer School 2005, Gothenburg,
in http://staff.math.su.se/palmgren/, 2005.
[82] E. Palmgren: Proof-relevance of families of setoids and identity in type theory, Arch. Math. Logic, 51,
2012, 35-47.
[83] E. Palmgren: Constructivist and structuralist foundations: Bishop's and Lawvere's theories
of sets, Annals of Pure and Applied Logic 163, 2012, 1384–1399.
[84] E. Palmgren: Bishop-style constructive mathematics in type theory - A tutorial, Slides, in
http://staff.math.su.se/palmgren/, 2013.
[85] E. Palmgren: Lecture Notes on Type Theory, 2014.
[86] E. Palmgren: On Equality of Objects in Categories in Constructive Type Theory, TYPES 2017, A. Abel
et. al. (Eds.), Article No. 7; pp. 7:1-7:7.
[87] E. Palmgren, O. Wilander: Constructing categories and setoids of setoids in type theory,
Logical Methods in Computer Science. 10 (2014), Issue 3, paper 25.
[88] I. Petrakis: Constructive Topology of Bishop Spaces, PhD Thesis,
Ludwig-Maximilians-Universität, München, 2015.
[89] I. Petrakis: Completely Regular Bishop Spaces, in A. Beckmann, V. Mitrana and M. Soskova (Eds.):
Evolving Computability, CiE 2015, LNCS 9136, 2015, 302–312.
[90] I. Petrakis: The Urysohn Extension Theorem for Bishop Spaces, in
S. Artemov and A. Nerode (Eds.) Symposium on Logical Foundations of Computer Science 2016,
LNCS 9537, Springer, 2016, 299–316.
[91] 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.
[92] 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.
[93] I. Petrakis: Constructive uniformities of pseudometrics and Bishop topologies,
Journal of Logic and Analysis 11:FT2, 2019, 1–44.
[94] 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.
[95] 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.
[94] I. Petrakis: A Yoneda lemma-formulation of the univalence axiom, manuscript, 2019, available at
[96] I. Petrakis: McShane-Whitney extensions in constructive analysis, Logical Methods in Computer
Science, Volume 16, Issue  2020, 18:1–18:23
[97] I. Petrakis: Embeddings of Bishop spaces, Journal of Logic and Computation,
exaa015, 2020, https://doi.org/10.1093/logcom/exaa015.
[98] I. Petrakis: Functions of Baire-class one over a Bishop topology, in M. Anselmo et. al. (Eds.)
Beyond the Horizon of Computability CiE 2020, Springer, LNCS 12098, 2020, 215-227.
[99] I. Petrakis: Proof-relevance in Bishop-style constructive mathematics, submitted, 2020.
[100] I. Petrakis: Bases of pseudocompact Bishop spaces, invited chapter in [28], to appear,
[101] I. Petrakis: Closed subsets in Bishop topological groups, submitted, 2021.

[103] I. Petrakis: Chu representations of categories related to constructive mathematics,
arXiv:2106.01878v1, 2021.
[104] I. Petrakis, M. Zeuner: Pre-measure spaces and pre-integration spaces in predicative Bishop-Cheng
measure theory, in preparation, 2021.
[105] M. Rathjen: Choice principles in constructive and classical set theories, Lecture
Notes in Logic 27, 2006, 299–326.
[106] M. Rathjen: The constructive Hilbert program and the limits of Martin-Löf Type Theory,
in S. Lindström et al. (Eds.) Logicism, Intuitionism, and Formalism: What has become of them?
Synthese Library Volume 341, Springer, 2009, 397–433.
[107] F. Richman: Constructive Mathematics, LNM 873, Springer-Verlag, 1981.
[108] F. Richman: Constructive mathematics without choice, in [116], pp.199–205.
[109] E. Rijke: Homotopy Type Theory, Master Thesis, Utrecht University, 2012.
[110] M. Rosenblatt (Ed.): Errett Bishop:
Reflections on Him and His Research, Contemporary Mathematics Volume 39, American Mathematical Society, 1985.
[111] K. A. Ross, K. Stromberg: Baire sets and Baire measures, Arkiv för Matematik Band 6 nr 8, 1965, 151–160.
[112] G. Sambin, J. M. Smith (Eds.): Twenty-five years of constructive type theory,
Oxford University Press, 1998.
[113] G. Sambin: The Basic Picture: Structures for Constructive Topology, Oxford University Press, 2020.
[114] N. Šanin: Constructive Real Numbers and Function Spaces,
Translations of Mathematical Monographs, vol. 21, AMS, Providence Rhode Island, 1968.
[115] M. Shulman: Linear Logic for Constructive Mathematics, arXiv:1805.07518v1, 2018.
[116] P. Schuster, U. Berger, H. Osswald (Eds.): Reuniting the Antipodes Constructive
and Nonstandard Views of the Continuum, Proc. 1999 Venice Symposium, Dordrecht: Kluwer, 2001.
[117] P. Schuster: Countable Choice as a Questionable Uniformity Principle, Philosophia Mathematica (3) Vol. 12, pp. 106–134, 2004.
[118] H. Schwichtenberg, S. Wainer: Proofs and Computations,  Perspectives in Logic,
Association for Symbolic Logic and Cambridge University Press, 2012.
[119] H. Schwichtenberg: Constructive analysis with witnesses, Lecture notes, LMU, 2019.
[120] I. Segal: Abstract probability spaces and a theorem of Kolmogoroff, Amer. J. Math. 76, 1954,
[121] I. Segal: Algebraic integration theory, Bull. Amer. Math. Soc. 71, 1965, 419–489.
[122] B. Spitters: Constructive and intuitionistic integration theory and functional analysis.
PhD Thesis, University of Nijmegen, 2002.
[123] B. Spitters: Constructive algebraic integration theory. Ann. Pure Appl. Logic 137(1-3), 2006,
[124] T. Streicher: Realizability, Lecture Notes, TU Darmstadt, 2018.
[125] S. J. Taylor: Introduction to Measure and Integration, Cambridge University Press, 1973.

[127] The Univalent Foundations Program: Homotopy Type Theory:
Univalent Foundations of Mathematics, Institute for Advanced Study, Princeton, 2013.
[128] A. S. Troelstra and D. van Dalen: Constructivism in Mathematics, Volume I, North-Holland, 1988.
[129] A. S. Troelstra and D. van Dalen: Constructivism in Mathematics, Volume II, North-Holland, 1988.
[130] A. Weil: Calcul des probabilités, méthode axiomatique, intégration, Revue Sci.
(Rev. Rose Illus.) 78, 1940, 201–208.
[131] T. Wiklund: Locally cartesian closed categories, coalgebras, and containers,
Uppsala Universitet, U.U.D.M Project Report, 2013:5.
[132] M. Zeuner: Families of Sets in Constructive Measure Theory, Master's Thesis, LMU, 2019.