Direct spectra of Bishop spaces and their limits

TL;DR

This paper develops the theory of direct and inverse limits of Bishop spaces within Bishop set theory, providing constructive proofs of fundamental theorems and duality principles in Bishop's constructive mathematics.

Contribution

It introduces the notions of spectra and limits of Bishop spaces and proves key theorems about their properties within an extended constructive framework.

Findings

Established the existence of direct limits of Bishop spaces.

Proved the fundamental theorems on inverse limits.

Demonstrated a duality principle between direct and inverse spectra.

Abstract

We apply fundamental notions of Bishop set theory (BST), an informal theory that complements Bishop's theory of sets, to the theory of Bishop spaces, a function-theoretic approach to constructive topology. Within BST we develop the notions of a direct family of sets, of a direct spectrum of Bishop spaces, of the direct limit of a direct spectrum of Bishop spaces, and of the inverse limit of a contravariant direct spectrum of Bishop spaces. Within the extension of Bishop's informal system of constructive mathematics BISH with inductive definitions with rules of countably many premises, we prove the fundamental theorems on the direct and inverse limits of spectra of Bishop spaces and the duality principle between them.

Equations

$$\forall_{x,y\in X}\big{(}[x=_{X}y\ \&\ P(x)]\Rightarrow P(y)\big{)}.$$

$$x\in X_P:\iff x\in X\&P(x),$$

$$1:=\{x\in \mathbb{N}\mid x{=}_{\mathbb{N}}0\}:=\{0\},$$

$$2:=\{x\in \mathbb{N}\mid x{=}_{\mathbb{N}}0\vee x{=}_{\mathbb{N}}1\}:=\{0,1\}.$$

$$D(X,{=}_X):=\{(x,y)\in X\times X\mid x{=}_{X}y\}.$$

$$f:=g:\Leftrightarrow\forall_{x\in X}\big{(}f(x):=g(x)\big{)}.$$

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

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

$$f=_{\mathbb{O}(X,Y)}g:\Leftrightarrow\forall_{x\in X}\big{(}f(x)=_{Y}g(x)\big{)}.$$

$$X=_{\mathbb{V}_{0}}Y:\Leftrightarrow\exists_{f\in\mathbb{F}(X,Y)}\exists_{g\in\mathbb{F}(Y,X)}\big{(}g\circ f=\mathrm{id}_{X}\ \&\ f\circ g=\mathrm{id}_{Y}\big{)}.$$

$$\Phi :{\text{bigcurlywedge}}_{i\in I}{\lambda }_0(i),$$

$$(f,g):A{=}_{\mathcal{P}(X)}B\Rightarrow (f,g):A{=}_{{\mathbb{V}}_0}B.$$

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

$$\forall_{i,j\in I}\big{(}\lambda_{0}(i)=_{\mathbb{V}_{0}}\lambda_{0}(j)\Rightarrow i=_{I}j\big{)}.$$

$$\Psi=_{\textnormal{{Map}}_{I}(\Lambda,M)}\Xi:\Leftrightarrow\forall_{i\in I}\big{(}\Psi_{i}=_{\mathbb{F}(\lambda_{0}(i),\mu_{0}(i))}\Xi_{i}\big{)}.$$

$$\mathrm{Id}_{\Lambda}:\bigcurlywedge_{i\in I}\mathbb{F}\big{(}\lambda_{0}(i),\lambda_{0}(i)\big{)},\ \ \ \mathrm{Id}_{\Lambda}(i):=\mathrm{id}_{\lambda_{0}(i)},\ \ \ i\in I,$$

$$\Lambda=_{\textnormal{{Fam}}(I)}M:\Leftrightarrow\exists_{\Phi\in\textnormal{{Map}}_{I}(\Lambda,M)}\exists_{\Xi\in\textnormal{{Map}}_{I}(M,\Lambda)}\big{(}\Phi\circ\Xi=\mathrm{id}_{M}\ \&\ \Xi\circ\Phi=\mathrm{id}_{\Lambda}\big{)}.$$

$$({\sigma }_0\circ h)(i):={\sigma }_0(h(i));i\in I,$$

$$({\sigma }_1\circ h{)}_{ij}:=({\sigma }_1\circ h)(i,j):{\sigma }_0(h(i))\to {\sigma }_0(h(j));(i,j)\in D(I),$$

$$({\sigma }_1\circ h{)}_{ij}:={\sigma }_{h(i)h(j)}.$$

$$w\in\sum_{i\in I}\lambda_{0}(i):\Leftrightarrow\exists_{i\in I}\exists_{x\in\lambda_{0}(i)}\big{(}w:=(i,x)\big{)},$$

$$(i,x){=}_{{\sum }_{i\in I}{\lambda }_0(i)}(j,y):\iff i{=}_{I}j\&{\lambda }_{ij}(x){=}_{{\lambda }_0(j)}y.$$

$$\Phi\in\prod_{i\in I}\lambda_{0}(i):\Leftrightarrow\Phi\in\mathbb{A}(I,\lambda_{0})\ \&\ \forall_{(i,j)\in D(I)}\big{(}\Phi_{j}=_{\lambda_{0}(j)}\lambda_{ij}(\Phi_{i})\big{)},$$

$${\lambda }_0^{X,Y}(0):=X\&{\lambda }_0^{X,Y}(1):=Y,\&{\lambda }_1^{X,Y}(0,0):={\mathrm{id}}_X\&{\lambda }_1^{X,Y}(1,1):={\mathrm{id}}_Y.$$

$${\text{pr}}_1^{\Lambda }(i,x):={\text{pr}}_1(i,x):=i,$$

$${\text{pr}}_2^{\Lambda }:{\text{bigcurlywedge}}_{(i,x)\in {\sum }_{i\in I}{\lambda }_0(i)}{\lambda }_0(i),$$

$${\text{pr}}_2^{\Lambda }(i,x):={\text{pr}}_2(i,x):=x,$$

$$\forall_{i,j,i{{}^{\prime}},j{{}^{\prime}}\in I}\big{(}i=_{I}i{{}^{\prime}}\ \&\ j=_{I}j{{}^{\prime}}\ \&\ i\preccurlyeq_{I}j\Rightarrow i{{}^{\prime}}\preccurlyeq_{I}j{{}^{\prime}}\big{)}.$$

$$\forall_{i,j\in I}\exists_{k\in I}\big{(}i\preccurlyeq_{I}k\ \&\ j\preccurlyeq_{I}k\big{)},$$

$$\forall_{i,j\in I}\exists_{k\in I}\big{(}i\succcurlyeq_{I}k\ \&\ j\succcurlyeq_{I}k\big{)}.$$

Full text

1. Introduction

1.1. Bishop’s set theory

The theory of sets underlying Bishop-style constructive mathematics $(\mathrm{BISH})$ was only sketched in Chapter 3 of Bishop’s seminal book [Bi67]. Since Bishop’s central aim in [Bi67] was to show that a large part of advanced mathematics can be done within a constructive and computational framework that does not contradict the classical practice, the inclusion of a detailed account of the set-theoretic foundations of $\mathrm{BISH}$ could possibly be against the effective delivery of his message.

The Bishop-Cheng measure theory, developed in [BC72], was very different from the measure theory of [Bi67], and the inclusion of an enriched version of the former into [BB85], the book on $\mathrm{BISH}$ that Bishop co-authored with Bridges later, affected the corresponding Chapter 3 in two main respects. First, the inductively defined notion of the set of Borel sets generated by a given family of complemented subsets of a set $X$, with respect to a set of real-valued functions on $X$, was excluded, as unnecessary, and, second, the operations on the complemented subsets of a set $X$ were defined differently, and in accordance to the needs of the new measure theory.

Yet, in both books many issues were left untouched, a fact that often was a source of confusion. In many occasions, especially in the measure theory of [BC72] and [BB85], the powerset was treated as a set, while in the measure theory of [Bi67], Bishop generally avoided the powerset by using appropriate families of subsets instead. In later works of Bridges and Richman, like  [BR87] and [MRR88], the powerset was clearly used as a set, in contrast though, to the predicative spirit of [Bi67]. The concept of a family of sets indexed by a (discrete) set, was asked to be defined in [Bi67] (Exercise 2, p. 72), and a definition, attributed to Richman, was given in [BB85] (Exercise 2, p. 78). An elaborate study of this concept within $\mathrm{BISH}$ is missing though, despite its central character in the measure theory of [Bi67], its extensive use in the theory of Bishop spaces [Pe15] and in abstract constructive algebra [MRR88]. Actually, in [MRR88] Richman introduced the more general notion of a family of objects of a category indexed by some set, but the categorical component in the resulting mixture of Bishop’s set theory and category theory was not explained in constructive terms111As it was done in the formulation of category theory in homotopy type theory (see Chapter 9 in [HoTT13])..

Bishop briefly discussed some formal aspects of $\mathrm{BISH}$ in [Bi70], where a variant of Gödel’s $T$ was proposed as a formal system for $\mathrm{BISH}$, while in his unpublished work [Bi68a] he elaborated a version of dependent type theory with one universe, in order to formalise $\mathrm{BISH}$. The various set-theoretic formalisations of $\mathrm{BISH}$, developed by Myhill [My75], Friedman [Fr77], Aczel [AR10], Feferman [Fe79], Beeson [Be81], and Greenleaf [Gr81], were, roughly speaking, quite influenced by Zermelo-Fraenkel set theory, and “top-down” approaches to $\mathrm{BISH}$, with many “unexpected” features222A detailed presentation of the unexpected features of these formalisations is going to be found in [Pe20]. with respect to its practice.

The type-theoretic interpretation of Bishop’s set theory into the theory of setoids (see especially the work of Palmgren [Pa05]-[PW14]) has become nowadays the standard way to understand Bishop sets. The identity type of Martin-Löf’s type theory ($\mathrm{MLTT}$) (see [ML98]), expresses, in a proof-relevant way, the existence of the least reflexive relation on a type, a fact with no counterpart in Bishop’s set theory. As a consequence, the free setoid on a type is definable (see [Pa14], p. 90), and the presentation axiom in setoids is provable. Moreover, in $\mathrm{MLTT}$ the families of types over a type $I$ form the type $I\to\mathcal{U}$, which belongs to the successor universe $\mathcal{U}{{}^{\prime}}$ of $\mathcal{U}$. In Bishop’s set theory though, where only one universe of sets is used, the set-character of the totality of all families of sets indexed by some set $I$ is questionable from the predicative point of view (see our comment after Definition 3).

1.2. Bishop Set Theory

Bishop set theory $(\mathrm{BST})$ is an informal, constructive theory of totalities and assignment routines that serves as a reconstruction of Bishop’s set theory. Its aim is, first, to fill in the “gaps” in Bishop’s account of the set theory underlying $\mathrm{BISH}$, and, second, to serve as an intermediate step between Bishop’s informal set theory and a suitable i.e., an adequate and faithful, in the sense of Feferman [Fe79], formalisation of $\mathrm{BISH}$. To assure faithfulness, we need to use concepts or principles that appear, explicitly or implicitly, in $\mathrm{BISH}$.

Next we describe briefly the features of $\mathrm{BST}$ that “complete” Bishop’s theory of sets in [Pe20].

1. Explicit use of a universe of sets. Bishop used a universe of sets only implicitly. E.g., he “roughly” describes in [Bi67], p. 72, a set-indexed family of sets as

$\ldots$ a rule which assigns to each $t$ in a discrete set $T$ a set $\lambda(t)$.

Every other rule, or assignment routine mentioned by Bishop is from one given totality, the domain of the rule, to some other totality, its codomain. The only way to make the rule of a family of sets compatible with this pattern is to employ a totality of sets. In the unpublished manuscript [Bi68a] Bishop explicitly used a universe in his formulation of dependent type theory as a formal system for $\mathrm{BISH}$. Here we use an open-ended totality $\mathbb{V}_{0}$ of sets, which contains the primitive set ${\mathbb{N}}$ and all defined (predicative) sets. $\mathbb{V}_{0}$ itself is not a set, but a class. It is a notion instrumental to the definition of dependent operations, and of a set-indexed family of sets.

2. Clear distinction between sets and classes. A class is a totality defined through a membership condition in which a quantification over $\mathbb{V}_{0}$ occurs. The powerset $\mathcal{P}(X)$ of a set $X$, the totality $\mathcal{P}^{\boldsymbol{]}\boldsymbol{[}}(X)$ of complemented subsets of a set $X$, and the totality $\mathcal{F}(X,Y)$ of partial functions from a set $X$ to a set $Y$ are characteristic examples of classes. A class is never used here as the domain of an assignment routine, but only as a codomain of an assignment routine.

3. Explicit use of dependent operations. The standard view, even among practicioners of Bishop-style constructive mathematicians, is that dependency is not necessary to $\mathrm{BISH}$. Dependent functions though, do appear explicitly in Bishop’s definition of the intersection $\bigcap_{t\in T}\lambda(t)$ of a family $\lambda$ of subsets of some set $X$ indexed by an inhabited set $T$ (see [Bi67], p. 65, and  [BB85], p. 70). As we try to show in [Pe20], the elaboration of dependency within $\mathrm{BISH}$ is only fruitful to it. Dependent functions are not only necessary to the definition of products of families of sets indexed by an arbitrary set, but in many areas of constructive mathematics. As already mentioned, dependency is formulated in Bishop’s type theory [Bi68a]. The somewhat “silent” role of dependency within Bishop’s set theory is replaced by a central role within $\mathrm{BST}$.

4. Elaboration of the theory of families of sets. With the use of the universe $\mathbb{V}_{0}$, of the notion of a non-dependent assignment routine $\lambda_{0}$ from an index-set $I$ to $\mathbb{V}_{0}$, and of a certain dependent operation $\lambda_{1}$, we define explicitly in Definition 3 the notion of a family of sets indexed by $I$. Although an $I$-family of sets is a certain function-like object, it can also be understood as an object with level the level of a set plus one. The corresponding notion of a “function” from an $I$-family $\Lambda$ to an $I$-family $M$ is that of a family-map. Operations between sets generate operations between families of sets and their family-maps. If the index-set $I$ is a directed set, the corresponding notion of a family of sets over it is that of a direct family of sets. Families of subsets of a given set $X$ over an index-set $I$ are special $I$-families that deserve an independent treatment. Families of equivalence classes, families of partial functions, families of complemented subsets and direct families of subsets are some of the variations of set-indexed families of subsets that are studied in [Pe20] with many applications in Bishop-style constructive mathematics.

Here we apply the general theory of families of sets, in order to develop the theory of spectra of Bishop spaces. A Bishop space is a constructive, function-theoretic alternative to the notion of a topological space. A Bishop topology $F$ on a set $X$ is a subset of the set $\mathbb{F}(X)$ of real-valued functions on $X$ that includes the constant functions and it is closed under addition, composition with Bishop continuous functions from ${\mathbb{R}}$ to ${\mathbb{R}}$, and uniform limits. Hence, in contrast to topological spaces, continuity of real-valued functions is a primitive notion and a concept of open set comes a posteriori. A Bishop topology on a set can be seen as an abstract and constructive approach to the ring of continuous functions $C(X)$ of a topological space $X$. Associating appropriately a Bishop topology to the set $\lambda_{0}(i)$ of a family of sets over a set $I$, for every $i\in I$, the notion of a spectrum of Bishop spaces is defined. If $I$ is a directed set, we get a direct spectrum. The theory of direct spectra of Bishop spaces and their limits is developed here in complete analogy to the classical theory of spectra of topological spaces and their limits (see [Du66], Appendix Two). The constructive theory of spectra of other structures, like groups, or rings, or modules, can be developed along the same lines.

1.3. Outline of this paper

We structure this paper333Here we continue our work in [Pe19d], where we showed the distributivity of dependent sums over dependent products within $\mathrm{BST}$ (there we used the acronym $\mathrm{CSFT}$ instead). as follows:

1. (1)

In Section 2 we present the fundamental notions of BST that are used in the subsequent sections. 2. (2)

In Section 3 we define the families of Bishop sets indexed by some set $I$ and the family-maps between them. The corresponding $\sum$-and $\prod$-sets are introduced. 3. (3)

In Section 4 we introduce the notion of a directed set with a modulus of directedness and the notion of a cofinal subset of a directed set with a modulus of cofinality. These moduli help us avoid the use of some choice-principle in later proofs. 4. (4)

In Section 5 we define the families of Bishop sets indexed by some directed set $(I,\preccurlyeq)$ and the family-maps between them. The corresponding $\sum^{\preccurlyeq}$-and $\prod^{\preccurlyeq}$-sets are introduced. 5. (5)

In Section 6 we include the basic notions and facts on Bishop spaces that are used in the subsequent sections. 6. (6)

In Section LABEL:sec:_direxternalspectra we define the notion of a direct spectrum of Bishop spaces, the notion of a continuous, direct spectrum-map, and we define a canonical Bishop topology on the direct sum of Bishop spaces. 7. (7)

In Section LABEL:sec:_fameqclass we define the families of subsets of a given set $X$ indexed by some set $I$, and the family-maps between them. We also define sets of subsets of a set $X$ indexed by some set $I$, and set-indexed families of equivalence classes of an equivalence structure. These notions are used in the definition of the direct limit of a (covariant) spectrum of Bishop spaces. 8. (8)

In Section LABEL:sec:_directlimit we define the direct limit $\underset{\to}{\mathrm{Lim}}\mathcal{F}_{i}$ of a direct spectrum of Bishop spaces, we prove the universal property of the direct limit for $\underset{\to}{\mathrm{Lim}}\mathcal{F}_{i}$ (Proposition LABEL:prp:_universaldirect), the existence of a unique map of the limit spaces from a spectrum-map (Theorem LABEL:thm:_directspectrummap1), the cofinality theorem for direct limits (Theorem LABEL:thm:_cofinal2), and the existence of a Bishop bijection for the product of spectra of Bishop spaces (Proposition LABEL:prp:_proddirect). 9. (9)

In Section LABEL:sec:_inverselimit we define the inverse limit $\underset{\leftarrow}{\mathrm{Lim}}\mathcal{F}_{i}$ of a contravariant direct spectrum of Bishop spaces, we prove the universal property of the inverse limit for $\underset{\leftarrow}{\mathrm{Lim}}\mathcal{F}_{i}$ (Proposition LABEL:prp:_universalinverse), the existence of a unique map of the limit spaces from a spectrum-map (Theorem LABEL:thm:_inverselimitmap), the cofinality theorem for inverse limits (Theorem LABEL:thm:_cofinal3), and the existence of a Bishop morphism for the product of inverse spectra of Bishop spaces (Proposition LABEL:prp:_prodinverse). 10. (10)

In Section LABEL:sec:_duality we prove the duality principle between the inverse and direct limits of Bishop spaces (Theorem LABEL:thm:_duality1).

The above results form a constructive counterpart to the theory of limits of topological spaces, as this is presented in [Du66], Appendix Two. As in the classic textbook of Dugundji, the choice of presentation is non-categorical and purely topological. By the first we mean that the language of category theory is avoided, and by the second, that the limit constructions are done directly for spaces. Our central aim is to present the basic theory of spectra of Bishop spaces within $\mathrm{BST}$. The use of categorical arguments would be consistent with our aim, only if the corresponding category theory was formulated within BST. In [MRR88] Richman used the notion of functor, to define the concept of a set-indexed family of sets. The problem with Richman’s approach was that the category theory involved was not explained in constructive terms, and its relation to $\mathrm{BISH}$ was left unclear. Here we avoid the use of categorical concepts in order to establish our results, as we want to work exclusively within BST. Actually, in [Pe20], pp. 80–83 we use the notion of a set-indexed family of sets in order to define the notion of a functor between small categories within $\mathrm{BST}$!

The theory of Bishop spaces, that was only sketched by Bishop in [Bi67], and revived by Bridges in [Br12], and Ishihara in [Is13], was developed by the author in [Pe15]-[Pe19c] and  [Pe20b],  [Pe20c]. Since it makes use of inductive definitions with rules of countably many premises, for their study we work within $\mathrm{BST}^{*}$, which is $\mathrm{BST}$ extended with such inductive definitions. Our concepts and results avoid the use even of countable choice (CC). Although practicioners of $\mathrm{BISH}$ usually embrace dependent choice, hence CC, 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 in [Ri01]. There are results in [BB85] that require CC in their proof, but we make no use of them here. E.g., our proofs of the cofinality theorems (Theorem LABEL:thm:_cofinal2 and Theorem LABEL:thm:_cofinal3) are choice-free as we use a proof-relevant definition of a cofinal subset. Notice that the formulation of the universal properties of the limits of spectra of Bishop spaces is impredicative, as it requires quantification over the class of Bishop spaces444A predicative formulation of a universal property can be given, if one is restricted to a given set-indexed family of Bishop spaces.. This is one reason we avoided the use of the universal properties in our proofs.

A formal system for $\mathrm{BISH}$ extended with such definitions is Myhill’s formal system $\mathrm{CST}^{*}$ where $\mathrm{CST}^{*}$ is Myhill’s extension of his formal system of constructive set theory $\mathrm{CST}$ with inductive definitions (see [My75]). A variation of $\mathrm{CST}^{*}$ is Aczel’s system CZF together with a weak version of Aczel’s regular extension axiom (REA), to accommodate these inductive definitions (see [AR10]).

For all basic facts on constructive analysis we refer to [BB85], for all results on Bishop spaces that are used here without proof we refer to [Pe15], and for all results on $\mathrm{BST}$ that are not shown here we refer to [Pe20].

2. Fundamentals of Bishop set theory

The logical framework of $\mathrm{BST}$ is first-order intuitionistic logic with equality (see [SW12], chapter 1). The primitive equality between terms is denoted by $s:=t$, and it is understood as a definitional, or logical, equality. I.e., we read the equality $s:=t$ as “the term $s$ is by definition equal to the term $t$”. If $\phi$ is an appropriate formula, for the standard axiom for equality $[a:=b\ \&\ \phi(a)]\Rightarrow\phi(b)$ we use the notation $[a:=b\ \&\ \phi(a)]:\Rightarrow\phi(b)$. The equivalence notation $:\Leftrightarrow$ is understood in the same way. The set $({\mathbb{N}},=_{{\mathbb{N}}},\neq_{{\mathbb{N}}})$ of natural numbers, where its canonical equality is given by $m=_{{\mathbb{N}}}n:\Leftrightarrow m:=n$, and its canonical inequality by $m\neq_{{\mathbb{N}}}n:\Leftrightarrow\neg(m=_{{\mathbb{N}}}n)$, is primitive. The standard Peano-axioms are associated to ${\mathbb{N}}$.

A global operation $(\cdot,\cdot)$ of pairing is also considered primitive. I.e., if $s,t$ are terms, their pair $(s,t)$ is a new term. The corresponding equality axiom is $(s,t):=(s{{}^{\prime}},t{{}^{\prime}}):\Leftrightarrow s:=s{{}^{\prime}}\ \&\ t:=t{{}^{\prime}}$. The $n$-tuples of given terms, for every $n$ larger than $2$, are definable. The global projection routines ${\rm Phys.~{}Rev.~{}B}_{1}(s,t):=s$ and ${\rm Phys.~{}Rev.~{}B}_{2}(s,t):=t$ are also considered primitive. The corresponding global projection routines for any $n$-tuples are definable.

An undefined notion of mathematical construction, or algorithm, or of finite routine is considered as primitive. The main objects of $\mathrm{BST}$ are totalities and assignment routines. Sets are special totalities and functions are special assignment routines, where an assignment routine is a special finite routine. All other equalities in $\mathrm{BST}$ are equalities on totalities defined though an equality condition. A predicate on a set $X$ is a bounded formula $P(x)$ with $x$ a free variable ranging through $X$, where a formula is bounded, if every quantifier occurring in it is over a given set.

{defi}

(i) *A primitive set $\mathbb{A}$ is a totality with a given membership $x\in\mathbb{A}$, and a given equality $x=_{\mathbb{A}}y$, that satisfies axiomatically the properties of an equivalence relation. The set ${\mathbb{N}}$ of natural numbers is the only primitive set considered here.

*(ii) *A $($non-inductive$)$defined totality $X$ is defined by a membership condition $x\in X:\Leftrightarrow\mathcal{M}_{X}(x),$ where $\mathcal{M}_{X}$ is a formula with $x$ as a free variable.

*(iii) *There is a special “open-ended” defined totality $\mathbb{V}_{0}$, which is called the universe of $($predicative$)$ sets. $\mathbb{V}_{0}$ is not defined through a membership-condition, but in an open-ended way. When we say that a defined totality $X$ is considered to be a set we “introduce” $X$ as an element of $\mathbb{V}_{0}$. We do not add the corresponding induction, or elimination principle, as we want to leave open the possibility of adding new sets in $\mathbb{V}_{0}$.

*(iv) *A defined preset $X$, or simply, a preset, is a defined totality $X$ the membership condition $\mathcal{M}_{X}$ of which expresses a construction.

*(v) *A defined totality $X$ with equality, or simply, a totality $X$ with equality is a defined totality $X$ equipped with an equality condition $x=_{X}y:\Leftrightarrow\mathcal{E}_{X}(x,y)$, where $\mathcal{E}_{X}(x,y)$ is a formula with free variables $x$ and $y$ that satisfies the conditions of an equivalence relation.

*(vi) *A defined set is a preset with a given equality, specified by a bounded formula.

*(vii) *A set is either a primitive set, or a defined set.

*(viii) *A totality is a class, if it is the universe $\mathbb{V}_{0}$, or if quantification over $\mathbb{V}_{0}$ occurs in its membership condition. *

{defi}

A bounded formula on a set $X$ is called an extensional property on $X$, if

[TABLE]

The totality $X_{P}$ generated by $P(x)$ is defined by $x\in X_{P}:\Leftrightarrow x\in X\ \&\ P(x)$,

[TABLE]

and the equality of $X_{P}$ is inherited from the equality of $X$. We also write $X_{P}:=\{x\in X\mid P(x)\}$, $X_{P}$ is considered to be a set, and it is called the extensional subset of $X$ generated by $P$.

Using the properties of an equivalence relation, it is immediate to show that an equality condition $\mathcal{E}_{X}(x,y)$ on a totality $X$ is an extensional property on the product $X\times X$ i.e., $[(x,y)=_{X\times X}(x{{}^{\prime}},y{{}^{\prime}})\ \&\ x=_{X}y]\Rightarrow x{{}^{\prime}}=_{X}y{{}^{\prime}}$. We consider the following extensional subsets of ${\mathbb{N}}$:

[TABLE]

[TABLE]

Since $n=_{{\mathbb{N}}}m:\Leftrightarrow n:=m$, the property $P(x):\Leftrightarrow x=_{{\mathbb{N}}}0\ \vee x=_{{\mathbb{N}}}1$ is extensional.

{defi}

If $(X,=_{X})$ is a set, its diagonal

is the extensional subset of $X\times X$

[TABLE]

If $=_{X}$ is clear from the context, we just write $D(X)$.

{defi}

Let $X,Y$ be totalities. A non-dependent assignment routine $f$ from $X$ to $Y$, in symbols $f\colon X\rightsquigarrow Y$, is a finite routine that assigns an element $y$ of $Y$ to each given element $x$ of $X$. In this case we write $f(x):=y$. If $g\colon X\rightsquigarrow Y$, let

[TABLE]

If $f:=g$, we say that $f$ and $g$ are definitionally equal. If $(X,=_{X})$ and $(Y,=_{Y})$ are sets, an operation from $X$ to $Y$ is a non-dependent assignment routine from $X$ to $Y$, while a function from $(X,=_{X})$ to $(Y,=_{Y})$, in symbols $f\colon X\to Y$, is an operation from $(X,=_{X})$ to $(Y,=_{Y})$ that respects equality i.e.,

[TABLE]

If $f\colon X\rightsquigarrow Y$ is a function from $X$ to $Y$, we say that $f$ is a function, without mentioning the expression “from $X$ to $Y$”. If $X$ is a set, the identity function $\mathrm{id}_{X}\colon X\to X$ is defined by the rule $x\mapsto x$, for every $x\in X$. A function $f\colon X\to Y$ is an embedding, in symbols $f\colon X\hookrightarrow Y$, if

[TABLE]

Let $X,Y$ be sets. The totality $\mathbb{O}(X,Y)$ of operations from $X$ to $Y$ is equipped with the following canonical equality:

[TABLE]

The totality $\mathbb{O}(X,Y)$ is considered to be a set. The set $\mathbb{F}(X,Y)$ of functions from $X$ to $Y$ is defined by separation on $\mathbb{O}(X,Y)$ through the extensional property P(f):\Leftrightarrow\forall_{x,x{{}^{\prime}}\in X}\big{(}x=_{X}x{{}^{\prime}}\Rightarrow f(x)=_{Y}f(x{{}^{\prime}})\big{)}. The equality $=_{\mathbb{F}(X,Y)}$ is inherited from $=_{\mathbb{O}(X,Y)}$.

The canonical equality on $\mathbb{V}_{0}$ is defined by

[TABLE]

In this case we write $(f,g):X=_{\mathbb{V}_{0}}Y$.

{defi}

Let $I$ be a set and $\lambda_{0}\colon I\rightsquigarrow\mathbb{V}_{0}$ a non-dependent assignment routine from $I$ to $\mathbb{V}_{0}$. A dependent operation $\Phi$ over $\lambda_{0}$, in symbols

[TABLE]

is an assignment routine that assigns to each element $i$ in $I$ an element $\Phi(i)$ in the set $\lambda_{0}(i)$. If $i\in I$, we call $\Phi(i)$ the $i$-component of $\Phi$, and we also use the notation $\Phi_{i}:=\Phi(i)$. An assignment routine is either a non-dependent assignment routine, or a dependent operation over some non-dependent assignment routine from a set to the universe. If $\Psi\colon\bigcurlywedge_{i\in I}\lambda_{0}(i)$, \Phi:=\Psi:\Leftrightarrow\forall_{i\in I}\big{(}\Phi_{i}:=\Psi_{i}\big{)}. If $\Phi:=\Psi$, we say that $\Phi$ and $\Psi$ are definitionally equal. Let $\mathbb{A}(I,\lambda_{0})$ be the totality of dependent operations over $\lambda_{0}$, equipped with the canonical equality \Phi=_{\mathbb{A}(I,\lambda_{0})}\Psi:\Leftrightarrow\forall_{i\in I}\big{(}\Phi_{i}=_{\lambda_{0}(i)}\Psi_{i}\big{)}. The totality $\mathbb{A}(I,\lambda_{0})$ is considered to be a set.

{defi}

If $X$ is a set, a subset of $X$ is a pair $(A,i_{A}^{X})$, where $A$ is a set and $i_{A}^{X}:A\hookrightarrow X$ is an embedding. If $(A,i_{A}^{X})$ and $(B,i_{B}^{X})$ are subsets of $X$, we say that $A$ is a subset of $B$, and we write $A\subseteq B$, if there is $f:A\to B$ such that the following diagram commutes

A$$B$$X.f$$i_{A}^{X}\$$\ i_{B}^{X}

In this case we write $f:A\subseteq B$, and usually we write $A$ instead of $(A,i_{A}^{X})$, and $i_{A}$ instead of $i_{A}^{X}$, if $X$ is clear from the context. The totality of the subsets of $X$ is the powerset $\mathcal{P}(X)$, and it is equipped with the equality $(A,i_{A})=_{\mathcal{P}(X)}(B,i_{B}):\Leftrightarrow A\subseteq B\ \&\ B\subseteq A$. If $f:A\subseteq B$ and $g:B\subseteq A$, we write $(f,g):A=_{\mathcal{P}(X)}B$. If $f:A\subseteq B$, then $f$ is an embedding: if $a,a{{}^{\prime}}\in A$ are such that $f(a)=_{B}f(a{{}^{\prime}})$, then $i_{B}(f(a))=_{X}i_{B}(f(a{{}^{\prime}}))\Leftrightarrow i_{A}(a)=_{X}i_{A}(a{{}^{\prime}})$, which implies $a=_{A}a{{}^{\prime}}$.

If $(f,g):A=_{\mathcal{P}(X)}B$, all the following diagrams commute

A$$B$$X.f$$g$$i_{A}^{X}\$$\ i_{B}^{X}

Moreover, the internal equality of subsets implies their external equality as sets i.e.,

[TABLE]

If $a\in A$, then $i_{A}(g(f(a)))=_{X}i_{B}(f(a))=_{X}i_{A}(a)$, hence $g(f(a))=_{A}a$, and $g\circ f=_{\mathbb{F}(A,A)}\mathrm{id}_{A}$. Similarly, $f\circ g=_{\mathbb{F}(B)}\mathrm{id}_{B}$. Since the membership condition of $\mathcal{P}(X)$ requires quantification over $\mathbb{V}_{0}$, the totality $\mathcal{P}(X)$ is a class. If $X_{P}$ is an extensional subset of $X$, then $(X_{P},i_{X_{P}})\subseteq X$, where $i_{X_{P}}\colon X_{P}\to X$ is defined by $x\mapsto x$, for every $x\in X_{P}$.

3. Set-indexed families of sets

An $I$-family of sets is an assignment routine $\lambda_{0}:I\rightsquigarrow\mathbb{V}_{0}$ that behaves like a function i.e., if $i=_{I}j$, then $\lambda_{0}(i)=_{\mathbb{V}_{0}}\lambda_{0}(j)$. The following definition is an exact formulation of this rough description555In [MRR88] Richman saw a set $I$ as a category with objects its elements and $\textnormal{{Hom}}_{=_{I}}(i,j):=\{x\in\{0\}\mid i=_{I}j\}$, for every $i,j\in I$. If we view $\mathbb{V}_{0}$ as a category with objects its elements and \textnormal{{Hom}}_{=_{\mathbb{V}_{0}}}(X,Y):=\big{\{}(f,f{{}^{\prime}}):\mathbb{F}(X,Y)\times\mathbb{F}(Y,X)\mid(f,f{{}^{\prime}}):X=_{\mathbb{V}_{0}}Y\big{\}}, for every $X,Y\in\mathbb{V}_{0}$, then an $I$-family of sets is a functor from the category $I$ to the category $\mathbb{V}_{0}$. Notice that in the definitions of $\textnormal{{Hom}}_{=_{I}}(i,j)$ and of $\textnormal{{Hom}}_{=_{\mathbb{V}_{0}}}(X,Y)$ the properties $P_{I}(x):=i=_{I}j$ and $Q_{X,Y}(f,f{{}^{\prime}}):=(f,f{{}^{\prime}}):X=_{\mathbb{V}_{0}}Y$ are extensional..

{defi}

If $I$ is a set, a family of sets indexed by $I$, or an $I$-family of sets, is a pair $\Lambda:=(\lambda_{0},\lambda_{1})$, where $\lambda_{0}:I\rightsquigarrow\mathbb{V}_{0}$, and666More accurately, we should write \lambda_{1}:\bigcurlywedge_{z\in D(I)}\mathbb{F}\big{(}\lambda_{0}(\textnormal{{pr}}_{1}(z)),\lambda_{0}(\textnormal{{pr}}_{2}(z))\big{)}.

[TABLE]

such that the following conditions hold:

$(a)$ For every $i\in I$, we have that $\lambda_{ii}:=\mathrm{id}_{\lambda_{0}(i)}$.

$(b)$ If $i=_{I}j$ and $j=_{I}k$, the following diagram commutes

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

If $i=_{I}j$, we call the function $\lambda_{ij}$ the transport map777We draw this term from MLTT. from $\lambda_{0}(i)$ to $\lambda_{0}(j)$. We call the assignment routine $\lambda_{1}$ the modulus of function-likeness of $\lambda_{0}$888Since $\lambda_{ii}=\lambda_{ji}\circ\lambda_{ij}$ and $\lambda_{jj}=\lambda_{ij}\circ\lambda_{ji}$, we have that $(\lambda_{ij},\lambda_{ji}):\lambda_{0}(i)=_{\mathbb{V}_{0}}\lambda_{0}(j)$.. An $I$-family of sets is called an $I$-set of sets, if

[TABLE]

If $A$ is a set, the constant $I$-family $A$ is the pair $\Lambda^{A}:=(\lambda_{0}^{A},\lambda_{1}^{A})$, where $\lambda_{0}(i):=A$, for every $i\in I$, and $\lambda_{1}(i,j):=\mathrm{id}_{A}$, for every $(i,j)\in D(I)$.

{defi}

Let $\Lambda:=(\lambda_{0},\lambda_{1})$ and $M:=(\mu_{0},\mu_{1})$ be $I$-families of sets. A family-map from $\Lambda$ to $M$ is a dependent operation999In the categorical setting of Richman, a family map $\Psi\in\textnormal{{Map}}_{I}(\Lambda,M)$ is a natural transformation from the functor $\Lambda$ to the functor $M$. In our view, the fact that the most fundamental concepts of category theory, that of a functor and of a natural transformation, are formulated in a natural way in $\mathrm{BST}$ through the notion of a dependent operation explains why category theory is so closely connected to $\mathrm{BST}$, or $\mathrm{MLTT}$. Both, $\mathrm{BST}$ and $\mathrm{MLTT}$, highlight the role of dependent operations. \Psi:\bigcurlywedge_{i\in I}\mathbb{F}\big{(}\lambda_{0}(i),\mu_{0}(i)\big{)}, such that for every $(i,j)\in D(I)$ the following diagram commutes

\mu_{0}(i)$$\mu_{0}(j).\lambda_{0}(j)$$\lambda_{0}(i)$$\mu_{ij}$$\lambda_{ij}$$\Psi_{i}$$\Psi_{j}

where $\Psi_{i}:=\Psi(i)$ is the $i$-component of $\Psi$, for every $i\in I$. We denote by $\textnormal{{Map}}_{I}(\Lambda,M)$ the totality of family-maps from $\Lambda$ to $M$, which is equipped with the equality

[TABLE]

We also write $\Phi:\Lambda\Rightarrow M$ to denote an element of $\textnormal{{Map}}_{I}(\Lambda,M)$. If $\Psi:\Lambda\Rightarrow M$ and $\Xi:M\Rightarrow N$, the composition family-map $\Xi\circ\Psi:\Lambda\Rightarrow N$ is defined by $(\Xi\circ\Psi)(i):=\Xi_{i}\circ\Psi_{i}$

\lambda_{0}(i)$$\lambda_{0}(j)$$\mu_{0}(j)$$\mu_{0}(i)$$\nu_{0}(i)$$\nu_{0}(j),\lambda_{ij}$$\Psi_{j}$$\mu_{ij}$$\Psi_{i}$$\Xi_{i}$$\Xi_{j}$$\nu_{ij}$$(\Xi\circ\Psi)_{i}\$$\ (\Xi\circ\Psi)_{j}

for every $i\in I$. The dependent operation

[TABLE]

is the identity family-map from $\Lambda$ to $\Lambda$. The totality of $I$-families is denoted by $\textnormal{{Fam}}(I)$, and

[TABLE]

The equalities on $\textnormal{{Map}}_{I}(\Lambda,M)$ and $\textnormal{{Fam}}(I)$ are equivalence relations. It is natural to accept the totality $\textnormal{{Map}}(\Lambda,M)$ as a set. If $\textnormal{{Fam}}(I)$ was a set though, the constant $I$-family with value $\textnormal{{Fam}}(I)$ would be defined though a totality in which it belongs to. From a predicative point of view, this cannot be accepted. The membership condition of the totality $\textnormal{{Fam}}(I)$ though, does not involve quantification over the universe $\mathbb{V}_{0}$, therefore it is also natural not to consider $\textnormal{{Fam}}(I)$ to be a class. Hence, $\textnormal{{Fam}}(I)$ is a totality “between” a (predicative) set and a class. For this reason, we say that $\textnormal{{Fam}}(I)$ is an impredicative set.

{defi}

If $K$ is a set, $\Sigma:=(\sigma_{0},\sigma_{1})$ is a $K$-family of sets and $h:I\to K$, the $h$-subfamily of $\Sigma$ is the pair $\Sigma\circ h:=(\sigma_{0}\circ h,\sigma_{1}\circ h)$, where

[TABLE]

[TABLE]

[TABLE]

Clearly, $\Sigma\circ h\in\textnormal{{Fam}}(I)$, and we write $(\Sigma\circ h)_{I}\leq\Sigma_{K}$.

{defi}

Let $\Lambda:=(\lambda_{0},\lambda_{1})$ be an $I$-family of sets. The101010For the sake of readability we denote the totalities of exterior union and dependent functions over $\Lambda$ only with reference to the assignment routine $\lambda_{0}$, while $\lambda_{1}$ is used in the equality formula of both totalities. In this way our notation is similar to the notation of the $\Sigma$-type and $\Pi$-type in $\mathrm{MLTT}$. exterior union, or disjoint union, $\sum_{i\in I}\lambda_{0}(i)$ of $\Lambda$ is defined by

[TABLE]

[TABLE]

The totality $\prod_{i\in I}\lambda_{0}(i)$ of dependent functions over $\Lambda$ is defined by

[TABLE]

and it is equipped with the equality of $\mathbb{A}(I,\lambda_{0})$.

The equalities on $\sum_{i\in I}\lambda_{0}(i)$ and $\prod_{i\in I}\lambda_{0}(i)$ are equivalence relations, and both these totalities are sets. If $X,Y$ are sets, let \Lambda(X,Y):=\big{(}\lambda_{0}^{X,Y},\lambda_{1}^{X,Y}\big{)} be the $\mathbb{2}$-family of $X$ and $Y$, where $\lambda_{0}^{X,Y}:\{0,1\}\rightsquigarrow\mathbb{V}_{0}$ is defined by

[TABLE]

It is easy to show that the dependent functions over $\Lambda(X,Y)$ are equal in $\mathbb{V}_{0}$ to $X\times Y$. The first projection on $\sum_{i\in I}\lambda_{0}(i)$ is the assignment routine $\textnormal{{pr}}_{1}^{\Lambda}:\sum_{i\in I}\lambda_{0}(i)\rightsquigarrow I$, defined by

[TABLE]

for every $(i,x)\in\sum_{i\in I}\lambda_{0}(i)$. It is immediate to show that $\textnormal{{pr}}_{1}^{\Lambda}$ is a function from $\sum_{i\in I}\lambda_{0}(i)$ to $I$. Moreover, it is easy to show that the pair $\Sigma^{\Lambda}:=(\sigma_{0}^{\Lambda},\sigma_{1}^{\Lambda})$, where $\sigma_{0}^{\Lambda}:\sum_{i\in I}\lambda_{0}(i)\rightsquigarrow\mathbb{V}_{0}$ is defined by $\sigma_{0}^{\Lambda}(i,x):=\lambda_{0}(i)$, and \sigma_{1}^{\Lambda}\big{(}(i,x),(j,y)\big{)}:=\lambda_{ij}, is a family of sets over $\sum_{i\in I}\lambda_{0}(i)$. The second projection on $\sum_{i\in I}\lambda_{0}(i)$ is the dependent operation

[TABLE]

[TABLE]

and it is a dependent function over $\Sigma^{\Lambda}$. The following facts are easy to show.

Proposition 1**.**

*Let $\Lambda:=(\lambda_{0},\lambda_{1})$, $M:=(\mu_{0},\mu_{1})\in\textnormal{{Fam}}(I)$, and $\Psi:\Lambda\Rightarrow M$.

$(i)$ For every $i\in I$ the assignment routine $e_{i}^{\Lambda}:\lambda_{0}(i)\rightsquigarrow\sum_{i\in I}\lambda_{0}(i)$, defined by $x\mapsto(i,x)$, is an embedding of $\lambda_{0}(i)$ into $\sum_{i\in I}\lambda_{0}(i)$.

$(ii)$ The assignment routine $\Sigma\Psi:\sum_{i\in I}\lambda_{0}(i)\rightsquigarrow\sum_{i\in I}\mu_{0}(i)$, defined by $\Sigma\Psi(i,x):=(i,\Psi_{i}(x))$, is a function from $\sum_{i\in I}\lambda_{0}(i)$ to $\sum_{i\in I}\mu_{0}(i)$, such that for every $i\in I$ the following diagram commutes*

\sum_{i\in I}\lambda_{0}(i)$$\sum_{i\in I}\mu_{0}(i).\mu_{0}(i)$$\lambda_{0}(i)$$\Sigma\Psi$$\Psi_{i}$$e_{i}^{\Lambda}$$e_{i}^{M}

$(iii)$* If $\Psi_{i}$ is an embedding, for every $i\in I$, then $\Sigma\Psi$ is an embedding.

$(iv)$ For every $i\in I$ the assignment routine $\pi_{i}^{\Lambda}:\prod_{i\in I}\lambda_{0}(i)\rightsquigarrow\lambda_{0}(i)$, defined by $\Theta\mapsto\Theta_{i},$ is a function from $\prod_{i\in I}\lambda_{0}(i)$ to $\lambda_{0}(i)$.

$(v)$ The assignment routine $\Pi\Psi:\prod_{i\in I}\lambda_{0}(i)\rightsquigarrow\prod_{i\in I}\mu_{0}(i)$, defined by $[\Pi\Psi(\Theta)]_{i}:=\Psi_{i}(\Theta_{i})$, for every $i\in I$, is a function from $\prod_{i\in I}\lambda_{0}(i)$ to $\prod_{i\in I}\mu_{0}(i)$, such that for every $i\in I$ the following diagram commutes*

\prod_{i\in I}\lambda_{0}(i)$$\prod_{i\in I}\mu_{0}(i).\mu_{0}(i)$$\lambda_{0}(i)$$\Pi\Psi$$\Psi_{i}$$\pi_{i}^{\Lambda}$$\pi_{i}^{M}

$(vi)$* If $\Psi_{i}$ is an embedding, for every $i\in I$, then $\Pi\Psi$ is an embedding.*

4. Directed sets

{defi}

Let $I$ be a set and $i\preccurlyeq_{I}j$ a binary extensional relation on $I$ i.e., an extensional property on $I\times I$

[TABLE]

If $i\preccurlyeq_{I}j$ is reflexive and transitive, then $(I,\preccurlyeq_{I})$ is called a a preorder. We call a preorder $(I,\preccurlyeq_{I})$ a directed set, and inverse-directed, respectively, if

[TABLE]

[TABLE]

The covariant diagonal $D^{\preccurlyeq}(I)$ of $\preccurlyeq_{I}$, the contravariant diagonal $D^{\succcurlyeq}(I)$ of $\preccurlyeq_{I}$, and the $\preccurlyeq_{I}$-upper set $I_{ij}^{\preccurlyeq}$ of $i,j\in I$ are defined, respectively, by

[TABLE]

[TABLE]

[TABLE]

As $i\preccurlyeq_{I}j$ is extensional, $D^{\preccurlyeq}(I),D^{\succcurlyeq}(I)$ are extensional subsets of $I\times I$, and $I_{ij}^{\preccurlyeq}$ of $I$.

{defi}

Let $(I,\preccurlyeq_{I})$ be a poset i.e., a preorder such that \big{[}i\preccurlyeq_{I}j\ \&\ j\preccurlyeq_{I}i\big{]}\Rightarrow i=_{I}j, for every $i,j\in I$. A modulus 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\preccurlyeq_{I}\delta(i,j)$ and $j\preccurlyeq_{I}\delta(i,j)$.

$(\delta_{2})$ If $i\preccurlyeq_{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,\preccurlyeq)$ is a directed set and $(J,e)\subseteq I$, where $e:J\hookrightarrow I$, and using for simplicity the same symbol $\preccurlyeq$, if we define $j\preccurlyeq j{{}^{\prime}}:\Leftrightarrow e(j)\preccurlyeq e(j{{}^{\prime}}),$ for every $j,j{{}^{\prime}}\in J$, then $(J,\preccurlyeq)$ 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\preccurlyeq j\big{)}, then $(J,\preccurlyeq)$ 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$.

{defi}

Let $(I,\preccurlyeq)$ be a directed set and $(J,e)\subseteq I$, and let $j\preccurlyeq j{{}^{\prime}}:\Leftrightarrow e(j)\preccurlyeq e(j{{}^{\prime}})$, for every $j,j{{}^{\prime}}\in J$. We say that $J$ is cofinal in $I$, if there is a function111111Categorically speaking, $e$ is a split monomorphism. $\textnormal{{cof}}_{J}:I\to J$, which we call a modulus of cofinality of $J$ in $I$, that satisfies the following conditions:

$(\textnormal{{Cof}}_{1})$ \forall_{j\in J}\big{(}\textnormal{{cof}}_{J}(e(j))=_{J}j\big{)}.

J$$I$$J.e$$\textnormal{{cof}}_{J}$$\mathrm{id}_{J}

$(\textnormal{{Cof}}_{2})$ \forall_{i,i{{}^{\prime}}\in I}\big{(}i\preccurlyeq i{{}^{\prime}}\Rightarrow\textnormal{{cof}}_{J}(i)\preccurlyeq\textnormal{{cof}}_{J}(i{{}^{\prime}})\big{)}.

$(\textnormal{{Cof}}_{3})$ \forall_{i\in I}\big{(}i\preccurlyeq e(\textnormal{{cof}}_{J}(i))\big{)}.

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

Taking into account the embedding $e$ of $J$ into $I$, condition $(\textnormal{{Cof}}_{3})$ is the exact writing of the classical defining condition \forall_{i\in I}\exists_{j\in J}\big{(}i\preccurlyeq j\big{)}. To add condition $(\textnormal{{Cof}}_{1})$ is natural, as $\preccurlyeq$ is reflexive. If we consider condition $(\textnormal{{Cof}}_{3})$ on $e(j)$, for some $j\in J$, then by condition $(\textnormal{{Cof}}_{1})$ we get $e(j)\preccurlyeq e(\textnormal{{cof}}_{J}(e(j)))=e(j)$. Condition $(\textnormal{{Cof}}_{2})$ is also harmless to add. In the classical setting if $i\preccurlyeq i{{}^{\prime}}$, and $j,j{{}^{\prime}}\in J$ such that $i\preccurlyeq j$ and $i{{}^{\prime}}\preccurlyeq j{{}^{\prime}}$, then there is some $i{{}^{\prime\prime}}\in I$ such that $j{{}^{\prime}}\preccurlyeq i{{}^{\prime\prime}}$ and $j\preccurlyeq i{{}^{\prime\prime}}$. If $i{{}^{\prime\prime}}\preccurlyeq j{{}^{\prime\prime}}$, for some $j{{}^{\prime\prime}}\in J$,

i$$j$$i{{}^{\prime}}$$j{{}^{\prime}}$$i{{}^{\prime\prime}}$$j{{}^{\prime\prime}}

then $j\preccurlyeq j{{}^{\prime\prime}}$. Since $i{{}^{\prime}}\preccurlyeq j{{}^{\prime\prime}}$ too, condition $(\textnormal{{Cof}}_{2})$ is justified. The added conditions $(\textnormal{{Cof}}_{1})$ and $(\textnormal{{Cof}}_{2})$ are used in the proofs of Theorem LABEL:thm:_cofinal2 and Lemma LABEL:lem:_cofinallemma(ii), respectively. Moreover, they are used in the proof of Theorem LABEL:thm:_cofinal3. The extensionality of $\preccurlyeq$ is also used in the proofs of Theorem LABEL:thm:_cofinal2 and Theorem LABEL:thm:_cofinal3.

E.g., if Even and Odd denote the sets of even and odd natural numbers, respectively, let $e\colon\textnormal{{Even}}\hookrightarrow{\mathbb{N}}$, defined by the identity map-rule, and $\textnormal{{cof}}_{\textnormal{{Even}}}\colon{\mathbb{N}}\to 2{\mathbb{N}}$, defined by the rule

[TABLE]

Then $(\textnormal{{Even}},e,\textnormal{{cof}}_{\textnormal{{Even}}})\subseteq{\mathbb{N}}$.

Remark 2**.**

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

Proof 4.1**.**

Let $j,j{{}^{\prime}}\in J$ and let $i\in I$ such that $e(j)\preccurlyeq i$ and $e(j{{}^{\prime}})\preccurlyeq i$. Since $i\preccurlyeq e(\textnormal{{cof}}_{J}(i))$, we get $e(j)\preccurlyeq e(\textnormal{{cof}}_{J}(i))$ and $e(j{{}^{\prime}})\preccurlyeq e(\textnormal{{cof}}_{J}(i))$ i.e., $j\preccurlyeq\textnormal{{cof}}_{J}(i)$ and $j{{}^{\prime}}\preccurlyeq\textnormal{{cof}}_{J}(i)$.

5. Direct families of sets

The next concept is a variation of the notion of a set-indexed family of sets121212A directed set $(I,\preccurlyeq_{I})$ can also be seen as a category with objects the elements of $I$, and $\textnormal{{Hom}}_{\preccurlyeq_{I}}(i,j):=\{x\in\{0\}\mid i\preccurlyeq_{I}j\}.$ If the universe $\mathbb{V}_{0}$ is seen as a category with objects its elements and $\textnormal{{Hom}}_{\preccurlyeq_{\mathbb{V}_{0}}}(X,Y):=\mathbb{F}(X,Y),$ an $(I,\preccurlyeq_{I})$-family of sets is a functor from the category $(I,\preccurlyeq_{I})$ to this new category $\mathbb{V}_{0}$.. A family of sets over a partial order is also used in the definition of a Kripke model for intuitionistic predicate logic, and the corresponding transport maps $\lambda_{ij}^{\preccurlyeq}$ are called transition functions (see [TD88], p. 85).

{defi}

Let $(I,\preccurlyeq_{I})$ be a directed set, and D^{\preccurlyeq}(I):=\big{\{}(i,j)\in I\times I\mid i\preccurlyeq_{I}j\big{\}} the diagonal of $\preccurlyeq_{I}$. A direct family of sets $(I,\preccurlyeq_{I})$, or an $(I,\preccurlyeq_{I})$-family of sets, is a pair $\Lambda^{\preccurlyeq}:=(\lambda_{0},\lambda_{1}^{\preccurlyeq})$, where $\lambda_{0}:I\rightsquigarrow\mathbb{V}_{0}$, and $\lambda_{1}^{\preccurlyeq}$, a modulus of transport maps for $\lambda_{0}$, where

[TABLE]

such that the transport maps $\lambda_{ij}^{\prec}$ of $\Lambda^{\preccurlyeq}$ satisfy the following conditions:

(a) *For every $i\in I$, we have that $\lambda_{ii}^{\preccurlyeq}:=\mathrm{id}_{\lambda_{0}(i)}$.

*(b) If $i\preccurlyeq_{I}j$ and $j\preccurlyeq_{I}k$, the following diagram commutes

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

If $X\in\mathbb{V}_{0}$, the constant $(I,\preccurlyeq_{I})$-family $X$ is the pair $C^{\preccurlyeq,X}:=(\lambda_{0}^{X},\lambda_{1}^{\preccurlyeq,X})$, where $\lambda_{0}^{X}(i):=X$, and $\lambda_{1}^{\preccurlyeq,X}(i,j):=\mathrm{id}_{X}$, for every $i\in I$ and $(i,j)\in D^{\preccurlyeq}(I)$.

Since in general $\preccurlyeq_{I}$ is not symmetric, the transport map $\lambda_{ij}^{\preccurlyeq}$ does not necessarily have an inverse. Hence $\lambda_{1}^{\preccurlyeq}$ is only a modulus of transport for $\lambda_{0}$, in the sense that determines the transport maps of $\Lambda^{\preccurlyeq}$, and not necessarily a modulus of function-likeness for $\lambda_{0}$.

{defi}

If $\Lambda^{\preccurlyeq}:=(\lambda_{0},\lambda_{1}^{\preccurlyeq})$ and $M^{\preccurlyeq}:=(\mu_{0},\mu_{1}^{\preccurlyeq})$ are $(I,\preccurlyeq_{I})$-families of sets, a direct family-map $\Phi$ from $\Lambda^{\preccurlyeq}$ to $M^{\preccurlyeq}$, denoted by $\Phi\colon\Lambda^{\preccurlyeq}\Rightarrow M^{\preccurlyeq}$, the set $\textnormal{{Map}}_{(I,\preccurlyeq_{I})}(\Lambda^{\preccurlyeq},M^{\preccurlyeq})$, and the totality $\textnormal{{Fam}}(I,\preccurlyeq_{I})$ of $(I,\preccurlyeq_{I})$-families are defined as in Definition 3. The direct sum $\sum_{i\in I}^{\preccurlyeq}\lambda_{0}(i)$ over $\Lambda^{\preccurlyeq}$ is the totality $\sum_{i\in I}\lambda_{0}(i)$ equipped with the equality

[TABLE]

The totality $\prod_{i\in I}^{\preccurlyeq}\lambda_{0}(i)$ of dependent functions over $\Lambda^{\preccurlyeq}$ is defined by

[TABLE]

and it is equipped with the equality of $\mathbb{A}(I,\lambda_{0})$.

Clearly, the property P(\Phi):\Leftrightarrow\forall_{(i,j)\in D^{\preccurlyeq}(I)}\big{(}\Phi_{j}=_{\lambda_{0}(j)}\lambda_{ij}^{\preccurlyeq}(\Phi_{i})\big{)} is extensional on $\mathbb{A}(I,\lambda_{0})$, the equality on $\prod_{i\in I}^{\preccurlyeq}\lambda_{0}(i)$ is an equivalence relation. $\prod_{i\in I}^{\preccurlyeq}\lambda_{0}(i)$ is considered to be a set.

Proposition 3**.**

The relation $(i,x)=_{\sum_{i\in I}^{\preccurlyeq}\lambda_{0}(i)}(j,y)$ is an equivalence relation.

Proof 5.1**.**

If $i\in I$, since $i\preccurlyeq_{I}i$, there is $k\in I$ such that $i\preccurlyeq_{I}k$, and by the reflexivity of the equality on $\lambda_{0}(k)$ we get $\lambda_{ik}^{\preccurlyeq}(x)=_{\lambda_{0}(k)}\lambda_{ik}^{\preccurlyeq}(x)$. The symmetry of $=_{\sum_{i\in I}^{\preccurlyeq}\lambda_{0}(i)}$ follows from the symmetry of the equalities $=_{\lambda_{0}(k)}$. To prove transitivity, we suppose that

[TABLE]

[TABLE]

and we show that

[TABLE]

By the definition of a directed set there is $k{{}^{\prime\prime}}\in I$ such that $k\preccurlyeq_{I}k{{}^{\prime\prime}}$ and $k{{}^{\prime}}\preccurlyeq_{I}k{{}^{\prime\prime}}$

i$$k$$j$$j{{}^{\prime}},k{{}^{\prime}}$$k{{}^{\prime\prime}}

hence by transitivity $i\preccurlyeq_{I}k{{}^{\prime\prime}}$ and $j{{}^{\prime}}\preccurlyeq_{I}k{{}^{\prime\prime}}$. Moreover,

[TABLE]

Notice that the projection operation from $\sum_{i\in I}^{\preccurlyeq}\lambda_{0}(i)$ to $I$ is not necessarily a function.

Proposition 4**.**

*If $(I,\preccurlyeq_{I})$ is a directed set, $\Lambda^{\preccurlyeq}:=(\lambda_{0},\lambda_{1}^{\preccurlyeq})$, $M^{\preccurlyeq}:=(\mu_{0},\mu_{1}^{\preccurlyeq})$ are $(I,\preccurlyeq_{I})$-families of sets, and $\Psi^{\preccurlyeq}:\Lambda^{\preccurlyeq}\Rightarrow M^{\preccurlyeq}$, the following hold.

*(i) *For every $i\in I$ the operation $e_{i}^{\Lambda^{\preccurlyeq}}:\lambda_{0}(i)\rightsquigarrow\sum_{i\in I}^{\preccurlyeq}\lambda_{0}(i)$, defined by $x\mapsto(i,x)$, for every $x\in\lambda_{0}(i)$, is a function from $\lambda_{0}(i)$ to $\sum_{i\in I}^{\preccurlyeq}\lambda_{0}(i)$.

*(ii) The operation $\Sigma^{\preccurlyeq}\Psi:\sum_{i\in I}^{\preccurlyeq}\lambda_{0}(i)\rightsquigarrow\sum_{i\in I}^{\preccurlyeq}\mu_{0}(i)$, defined by \big{(}\Sigma^{\preccurlyeq}\Psi\big{)}(i,x):=(i,\Psi_{i}(x)), for every $(i,x)\in\sum_{i\in I}^{\preccurlyeq}\lambda_{0}(i)$, is a function from $\sum_{i\in I}^{\preccurlyeq}\lambda_{0}(i)$ to $\sum_{i\in I}^{\preccurlyeq}\mu_{0}(i)$ such that, for every $i\in I$, the following left diagram commutes

\sum_{i\in I}^{\preccurlyeq}\lambda_{0}(i)$$\sum_{i\in I}^{\preccurlyeq}\mu_{0}(i)$$\mu_{0}(i)$$\lambda_{0}(i)$$\prod_{i\in I}^{\preccurlyeq}\lambda_{0}(i)$$\prod_{i\in I}^{\preccurlyeq}\mu_{0}(i).\mu_{0}(i)$$\lambda_{0}(i)$$\Sigma^{\preccurlyeq}\Psi$$\Psi_{i}$$e_{i}^{\Lambda^{\preccurlyeq}}$$e_{i}^{M^{\preccurlyeq}}$$\Pi^{\preccurlyeq}\Psi$$\Psi_{i}$$\pi_{i}^{\Lambda^{\preccurlyeq}}$$\pi_{i}^{M^{\preccurlyeq}}

(iii) *If $\Psi_{i}$ is an embedding, for every $i\in I$, then $\Sigma^{\preccurlyeq}\Psi$ is an embedding.

*(iv) *For every $i\in I$ the operation $\pi_{i}^{\Lambda^{\preccurlyeq}}:\prod_{i\in I}^{\preccurlyeq}\lambda_{0}(i)\rightsquigarrow\lambda_{0}(i)$, defined by $\Theta\mapsto\Theta_{i}$, for every $\Theta\in\prod_{i\in I}^{\preccurlyeq}\lambda_{0}(i)$, is a function from $\prod_{i\in I}^{\preccurlyeq}\lambda_{0}(i)$ to $\lambda_{0}(i)$.

*(v) *The operation $\Pi^{\preccurlyeq}\Psi:\prod_{i\in I}^{\preccurlyeq}\lambda_{0}(i)\rightsquigarrow\prod_{i\in I}^{\preccurlyeq}\mu_{0}(i)$, defined by $[\Pi^{\preccurlyeq}\Psi(\Theta)]_{i}:=\Psi_{i}(\Theta_{i})$, for every $i\in I$ and $\Theta\in\prod_{i\in I}^{\preccurlyeq}\lambda_{0}(i)$, is a function from $\prod_{i\in I}^{\preccurlyeq}\lambda_{0}(i)$ to $\prod_{i\in I}^{\preccurlyeq}\mu_{0}(i)$, such that, for every $i\in I$, the above right diagram commutes.

*(vi) If $\Psi_{i}$ is an embedding, for every $i\in I$, then $\Pi^{\preccurlyeq}\Psi$ is an embedding.

Proof 5.2**.**

*(i) Let $x,y\in\lambda_{0}(i)$ with $x=_{\lambda_{0}(i)}y$. As $\preccurlyeq$ is reflexive, if we take $k:=i$, we get $\lambda_{ii}^{\preccurlyeq}(x):=\mathrm{id}_{\lambda_{0}(i)}(x):=x=_{\lambda_{0}(i)}y=:\mathrm{id}_{\lambda_{0}(i)}(y)=:\lambda_{ii}^{\preccurlyeq}(y)$, hence $(i,x)=_{\sum_{i\in I}^{\preccurlyeq}\lambda_{0}(i)}(i,y)$.

(ii) If $(i,x)=_{\sum_{i\in I}^{\preccurlyeq}\lambda_{0}(i)}(j,y)$, there is $k\in I$ such that $i\preccurlyeq_{I}k$, $j\preccurlyeq_{I}k$ and $\lambda_{ik}^{\preccurlyeq}(x)=_{\lambda_{0}(k)}\lambda_{jk}^{\preccurlyeq}(y)$. We show the following equality:*

[TABLE]

If we take $k{{}^{\prime}}:=k$, by the commutativity of the following diagrams, and since $\Psi_{k}$ is a function,

\mu_{0}(i)$$\mu_{0}(k)$$\lambda_{0}(k)$$\lambda_{0}(i)$$\mu_{0}(j)$$\lambda_{0}(j)$$\mu_{0}(k)$$\lambda_{0}(k)$$\mu_{ik}^{\preccurlyeq}$$\lambda_{ik}^{\preccurlyeq}$$\Psi_{i}$$\Psi_{k}$$\mu_{jk}^{\preccurlyeq}$$\lambda_{jk}^{\preccurlyeq}$$\Psi_{j}$$\Psi_{k}

[TABLE]

*(iii) If we suppose \big{(}\Sigma^{\preccurlyeq}\Psi\big{)}(i,x)=_{{\sum_{i\in I}^{\preccurlyeq}\mu_{0}(i)}}\big{(}\Sigma^{\preccurlyeq}\Psi\big{)}(j,y) i.e., \mu_{ik}^{\preccurlyeq}(\Psi_{i}(x))=_{\mu_{0}(k)}\mu_{jk}^{\preccurlyeq}(\Psi_{j}(y))\big{)}, for some $k\in I$ with $i,j\preccurlyeq_{I}k$, by the proof of case (ii) we get \Psi_{k}\big{(}\lambda_{ik}^{\preccurlyeq}(x)\big{)}=_{\mu_{0}(k)}\Psi_{k}\big{(}\lambda_{jk}^{\preccurlyeq}(y)\big{)}, and since $\Psi_{k}$ is an embedding, we get $\lambda_{ik}^{\preccurlyeq}(x)=_{\lambda_{0}(k)}\lambda_{jk}^{\preccurlyeq}(y)$ i.e., $(i,x)=_{\sum_{i\in I}^{\preccurlyeq}\lambda_{0}(i)}(j,y)$.

(iv)-(vi) Their proof is omitted, since a proof of their contravariant version131313In a contravariant family the transport maps are of type $\lambda_{0}(j)\to\lambda_{0}(i)$, if $i\preccurlyeq j$. is given in the proof of Theorem LABEL:thm:_inverselimitmap.*

Since the transport functions $\lambda_{ik}^{\preccurlyeq}$ are not in general embeddings, we cannot show in general that $e_{i}^{\Lambda^{\preccurlyeq}}$ is an embedding, as it is the case for the map $e_{i}^{\Lambda}$ in Proposition 1(i).

6. On Bishop spaces

From now on we work within the extension $\mathrm{BST}^{*}$ of $\mathrm{BST}$.

{defi}

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

[TABLE]

for every $\epsilon>0$ and every $n\in{\mathbb{N}}^{+}$. We denote by $\mathrm{Bic}({\mathbb{R}})$ the set of continuous functions from ${\mathbb{R}}$ to ${\mathbb{R}}$, which is equipped with the equality inherited from $\mathbb{F}({\mathbb{R}})$.

We could have defined the modulus of continuity $\omega_{\phi,n}$ as a function from ${\mathbb{N}}^{+}$ to ${\mathbb{N}}^{+}$. A continuous function $\phi\colon{\mathbb{R}}\to{\mathbb{R}}$ is uniformly continuous on every bounded subset of ${\mathbb{R}}$. The latter is an impredicative formulation of uniform continuity, as it requires quantification over the class $\mathcal{P}({\mathbb{R}})$. The formulation of uniform continuity in the Definition 6 though, is predicative, since it requires quantification over the sets ${\mathbb{N}}^{+},\mathbb{F}({\mathbb{R}}^{+},{\mathbb{R}}^{+})$ and $[-n,n]$.

{defi}

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

[TABLE]

[TABLE]

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

[TABLE]

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

{defi}

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

$(\mathrm{BS}_{1})$ If $a\in{\mathbb{R}}$, then $\overline{a}^{X}\in 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$

X$${\mathbb{R}}$${\mathbb{R}}.f$$F\ni\phi\circ f\$$\phi\in\mathrm{Bic}({\mathbb{R}})

$(\mathrm{BS}_{4})$ $\overline{F}=F$.

If $F$ is inhabited, then $(\mathrm{BS}_{1})$ is provable by $(\mathrm{BS}_{3})$. The set of constant functions $\mathrm{Const}(X)$ is the trivial topology on $X$, while $\mathbb{F}(X)$ is the discrete topology on $X$. Clearly, if $F$ is a topology on $X$, then $\mathrm{Const}(X)\subseteq F\subseteq\mathbb{F}(X)$, and the set of its bounded elements $F^{*}$ is also a topology on $X$. We denote by $\mathcal{F}^{*}:=(X,F^{*})$ the Bishop space of bounded elements of a Bishop topology $F$. It is easy to see that the pair $\mathcal{R}:=({\mathbb{R}},\mathrm{Bic}({\mathbb{R}}))$ is a Bishop space, which we call the Bishop space of reals. A Bishop topology $F$ is a ring and a lattice; since $|\mathrm{id}_{{\mathbb{R}}}|\in\mathrm{Bic}({\mathbb{R}})$, where $\mathrm{id}_{{\mathbb{R}}}$ is the identity function on ${\mathbb{R}}$, by BS3, if $f\in F$, then $|f|\in F$. By BS2 and BS3, and using the following equalities

[TABLE]

[TABLE]

[TABLE]

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 [Bi67], p. 72, the least topology including a given subbase $F_{0}$. This inductive definition, which is also found in [BB85], p. 78, is crucial to the definition of new Bishop topologies from given ones.

{defi}

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

[TABLE]

[TABLE]

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

The last, most complex rule above can be replaced by the rule

[TABLE]

a rule with countably many premisses. The corresponding induction principle $\mathrm{Ind}_{\bigvee F_{0}}$ is

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

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

{defi}

If $\mathcal{F}:=(X,F)$ and $\mathcal{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)$

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

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

[TABLE]

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

X$$Y$${\mathbb{R}}.h$$F\ni g_{0}\circ h\ \$$g_{0}\in G_{0}

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

{defi}

Let $\mathcal{F}:=(X,F),\mathcal{G}:=(Y,G)$ be Bishop spaces, $(A,i_{A})\subseteq X$ inhabited, and $\phi:X\rightarrow Y$ a surjection. The product Bishop space $\mathcal{F}\times\mathcal{G}:=(X\times Y,F\times G)$ of $\mathcal{F}$ and $\mathcal{G}$, the relative Bishop space ${\mathbb{F}}_{|A}:=(A,F_{|A})$ on $A$, and the pointwise exponential Bishop space