Families of Sets in Bishop Set Theory

Iosif Petrakis

Mathematics Institute, Ludwig-Maximilians-Universität München

CHAPTER: ABSTRACT

We develop the theory of set-indexed families of sets within the informal Bishop Set Theory $(\BST)$, a
reconstruction of Bishop's theory of sets,. The latter is the informal theory of sets and functions underlying
Bishop-style constructive mathematics $(\BISH)$ and it is developed in Chapter 3 of Bishop's seminal
book Foundations of Constructive Analysis [9] and in Chapter
3 of Constructive Analysis [19] that Bishop co-authored with Bridges.

In the Introduction we briefly present the relation of Bishop's set theory to the set-theoretic
and type-theoretic foundations of mathematics, and we describe the features of $\BST$ that “complete”
Bishop's theory of sets. These are the explicit use of the class “universe of sets”, a clear distinction
between sets and classes, the explicit use of dependent operations, and the concrete formulation of
various notions of families of sets.

In Chapter <ref> we present the fundamentals of Bishop's theory of sets, extended with the features which form $\BST$. The universe $\D V_0$ of sets is implicit in Bishop's work, while the notion of a dependent operation
over a non-dependent assignment routine from a set to $\D V_0$ is explicitly mentioned, although in a rough way.
These concepts are necessary to a concrete definition of a set-indexed family of sets,
the main object of our study, which is only mentioned by Bishop.

In Chapter <ref> we develop the basic theory of set-indexed families of sets and of
family-maps between them. We study the exterior union of a family of sets $\Lambda$, or the $\sum$-set of
$\Lambda$, and the set
of dependent functions over $\Lambda$, or the $\prod$-set of $\Lambda$. We prove the distributivity of
$\prod$ over $\sum$ for families of sets indexed by a product of sets, which is the translation
of the type-theoretic axiom of choice into $\BST$. Sets of sets are special set-indexed families of sets
that allow “lifting” of functions on the index-set to functions on them. The direct families of sets and the
set-relevant families of sets are introduced. The index-set of the former is a directed set, while the
transport maps of the latter are more than one and appropriately indexed. With the use of the introduced universe
$\D V_0^{\im}$ of sets and impredicative sets we study families of families of sets, the next rung of the
ladder of set-like objects in $\D V_0^{\im}$.

In Chapter <ref> we develop the basic theory of set-indexed families of subsets
and of the corresponding family-maps between them. In contrast to set-indexed families of sets, the properties
of which are determined “externally” through their transport maps, the properties of a set-indexed family
$\Lambda(X)$ of subsets of a given set $X$ are determined “internally” through the embeddings of the
subsets of $\Lambda(X)$ to $X$. The interior union of $\Lambda(X)$ is the internal analogue to the $\sum$-set
of a set-indexed family of sets $\Lambda$,
and the intersection of $\Lambda(X)$ is the internal analogue to the $\prod$-set of $\Lambda$.
Families of sets over products, sets of subsets, and direct families of subsets are the internal analogue to the
corresponding notions for families of sets. Set-indexed families of partial functions
and set-indexed families of complemented subsets, together with their corresponding family-maps, are studied.

In Chapter <ref> we connect various notions and results from the theory of families of sets
and subsets to the theory of Bishop spaces, a function-theoretic approach to constructive topology. Associating
in an appropriate way to each set $\lambda_0(i)$ of an $I$-family of sets $\Lambda$ a Bishop topology $F_i$, a
spectrum $S(\Lambda)$ of Bishop spaces is generated. The $\sum$-set and the $\prod$-set of a spectrum $S(\Lambda)$
are equipped with canonical Bishop topologies. A direct spectrum of Bishop spaces is a family of Bishop spaces
associated to a direct family of sets. The direct and inverse limits of direct spectra of Bishop spaces are studied.
Direct spectra of Bishop subspaces are also examined. Many Bishop topologies used in this chapter are defined inductively within the extension $\BISH^*$ of $\BISH$ with inductive definitions with rules of countably many premises.

In Chapter <ref> we study the Borel and Baire sets within Bishop spaces as a constructive
counterpart to the study of Borel and Baire algebras within topological spaces. As we use the inductively
defined least Bishop topology, and as the Borel and Baire sets over a family of $F$-complemented subsets are
defined inductively, we work again within $\BISH^*$. In contrast to the classical theory, we show that
the Borel and the Baire sets of a Bishop space coincide. Finally, our reformulation within $\BST$ of the Bishop-Cheng
definition of a measure space and of an integration space, based on the notions of families of complemented
subsets and of families of partial functions, facilitates a predicative reconstruction of the originally
impredicative Bishop-Cheng measure theory.

CHAPTER: INTRODUCTION

Bishop's theory of sets is Bishop's account of the informal theory of sets and functions that underlies
Bishop-style constructive mathematics $\BISH$. We briefly present the relation of this theory to
the set-theoretic and type-theoretic foundations of mathematics. Bishop Set Theory $(\BST)$ is
our “completion” of Bishop's theory of sets
with a universe of sets, with a clear distinction between sets and classes, with an explicit use
of dependent operations, and with a concrete formulation  of various notions of families of sets.
We explain how the theory of families of sets within $\BST$ that is elaborated in this work is used,
in order to reveal proof-relevance in $\BISH$, to develop the theory of spectra of Bishop spaces, and
to reformulate predicatively the fundamental notions of the impredicative Bishop-Cheng measure theory.

§ BISHOP'S THEORY OF SETS

The theory of sets underlying Bishop-style constructive mathematics $(\BISH)$ was only sketched in Chapter 3 of
Bishop's seminal book [9]. Since Bishop's central aim in [9] 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 $\BISH$ could possibly be against the effective
delivery of his message.

The Bishop-Cheng measure theory, developed in [18], was very
different from the measure theory of [9], and the inclusion of an enriched version of the former
into [19], the book on constructive analysis 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 [18] and [19], the powerset was treated as a set, while in the
measure theory of [9], Bishop generally avoided the powerset by using appropriate families of
subsets instead. In later works of Bridges and Richman, like  [20] and [76], the powerset was
clearly used as a set, in contrast though, to the predicative spirit of [9].

The concept of a family of
sets indexed by a (discrete) set, was asked to be defined in [9] (Exercise 2, p. 72), and a definition,
attributed to Richman, was given in [19] (Exercise 2, p. 78). An elaborate study though, of this concept
within $\BISH$ is missing, despite its central character in the measure theory of [9], its
extensive use in the theory of Bishop spaces [88] and in abstract constructive algebra [76].
Actually, in [76] 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 terms[This was done e.g., in the
the formulation of category theory in homotopy type theory (Chapter 9 in [127]).].

Contrary to the standard view on Bishop's relation to formalisation, Bishop was very interested in it.
In [12], p. 60, he writes:

Another important foundational problem is to find a formal system that will efficiently
express existing predictive mathematics. I think we should keep the formalism as primitive as possible,
starting with a minimal system and enlarging it only if the enlargement serves a genuine mathematical
need. In this way the formalism and the mathematics will hopefully interact to the advantage
of both.

Actually, in [12] Bishop proposed $\Sigma$, a variant
of Gödel's $T$, as a formal system for $\BISH$. In the last two pages of [12] he sketched very
briefly how $\Sigma$ can be presented as a functional programming language, like fortran and algol.
In p. 72 he also added:

It would be interesting to take $\Sigma$ as the point of departure for a reasonable programming language,
and to write a compiler.

Bishop's views on a full-scale program on the foundations of mathematics are realised in a more developed
form in his, unfortunately, unpublished papers [10] and [11]. In the first, Bishop elaborated
a version of dependent type theory with one universe, in order to formalise $\BISH$. This was the first time that  some form of type theory is used to formalise constructive mathematics.

As Martin-Löf explains in [71], p. 13, he got access to Bishop's book only shortly after his own book
on constructive mathematics [71] was finished. Bishop's book [9] also motivated his version of type theory.
Martin-Löf opened his first published paper on type theory ([72], p. 73) as follows.

The theory of types with which we shall be concerned is intended to be a full scale system for formalizing
intuitionistic mathematics as developed, for example, in the book of Bishop.

The type-theoretic interpretation of Bishop's set theory into the theory of setoids (see especially the
work of Palmgren [81]-[87]) has become nowadays the standard way to understand Bishop sets
(as far as I know, this is a term due to Palmgren). A setoid is a type $A$ in a fixed universe $\C U$ equipped
with a term $\simeq \colon A \to A \to \C U$ that satisfies the properties of an equivalence relation. The identity
type of Martin-Löf's intensional type theory ($\MLTT$) (see [74]), 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 [85], p. 90), and the presentation axiom in
setoids is provable (see Note <ref>). Moreover, in $\MLTT$ the families of types over a type $I$ is the type $I \to \C U$,
which belongs to the successor universe $\C U{'}$ of $\C U$. In Bishop's set theory though, where only one
universe of sets is implicitly 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 the Definition <ref>).

The quest $\B Q$$\B Q$ of finding a formal system suitable for Bishop's system of informal constructive
mathematics $\BISH$ dominated the foundational studies of the 1970's. Myhill's system $\CST$,
introduced in [80], and later Aczel's $\CZF$ (see [1]),
Friedman's system $B$, developed in [51], and Feferman's system of explicit mathematics $T_0$
(see [48] and [49]), are some of the systems related to $\B Q$,
but soon developed independently from it. These systems
were influenced a lot from the classical Zermelo-Fraenkel set theory, and could be described as “top-down”
approaches to the goal of $\B Q$, as they have many “unexpected” features with respect to
Using Feferman's terminology from [49], these formal systems are not completely
faithfulfaithful formalisation to $\BISH$. If $T$ is a formal theory of an informal body of mathematics $M$,
Feferman gave in [49] the following definitions.

(i) $T$ is adequate for $M$, if every concept, argument,adequate formalisation
and result of $M$ is represented by a (basic or defined) concept, proof, and a theorem, respectively, of $T$.

(ii) $T$ is faithful to $M$, if every basic concept of $T$ corresponds to a basic concept of $M$ and every
and rule of $T$ corresponds to or is implicit in the assumptions and reasoning followed in $M$ (i.e., $T$
does not go beyond $M$ conceptually or in principle).

In [5], p. 153, Beeson called $T$ suitable to $M$, if $T$ is adequate for $M$ and faithful to $M$.

Beeson's systems $S$ and $S_0$ in [5], and Greenleaf's system
of liberal constructive set theory $\LCST$ in [55] were dedicated to $\B Q$. Especially Beeson tried to
find a faithful and adequate formalisation of $\BISH$, and, by including a serious amount of proof relevance,
his systems stand in between the set-theoretic, proof-irrelevant point of view and the type-theoretic,
proof-relevant point of view.

All aforementioned systems though, were not really “tested” with respect to $\BISH$. Only very small parts of $\BISH$
were actually implemented in them, and their adequacy for $\BISH$ was mainly a claim, rather than
a shown fact. The implementation of Bishop's constructivism within a formal system for it was taken seriously
in the type-theoretic formalisations of $\BISH$, and especially in the work of Coquand (see e.g., [37]
and [40]), Palmgren (see e.g., [62] and the collaborative  work [39]), the
Nuprl research group of Constable (see e.g., [36]), and of Sambin and Maietti
within the Minimalist Foundation (see [113] and [70]).

§ BISHOP SET THEORY $(\BST)$ AND BISHOP'S THEORY OF SETS

Bishop set theory $(\BST)$ is an informal, constructive theory of totalities and assignment routines
that serves as a “completion” of Bishop's theory of sets. Its first aim is to fill in the “gaps”, or
highlight the fundamental notions that were suppressed by Bishop in his account of the set theory underlying $\BISH$.
Its second aim is
to serve as an intermediate step between Bishop's theory of sets and a suitable, in Beeson's sense, formalisation of
$\BISH$. To assure faithfulness, we use concepts or principles that appear, explicitly or implicitly, in $\BISH$.
Next we describe briefly the features of $\BST$ that “complete” Bishop's theory of sets.

1. Explicit use of a universe of sets. Bishop used a universe of sets only implicitly. E.g., he “roughly”
describes in [9], 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 [10] Bishop explicitly used a universe in his type theory.
Here we use the totality $\D V_0$ of sets, which is defined in an open-ended way,  and it contains the primitive
set $\Nat$ and all defined sets. $\D 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 $\D V_0$ occurs. The powerset $\C P(X)$ of a set $X$, the totality $\C P^{\Disj}(X)$
of complemented subsets of a set $X$, and the totality $\C 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, 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 $\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 [9], p. 65, and  [19], p. 70). We show that the elaboration of dependency within $\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 as we show throughout this work in many areas of constructive mathematics.
Some form of dependency is also formulated in Bishop's type theory [10]. The somewhat “silent” role of
dependency within Bishop's set theory is replaced by a central role within $\BST$.

4. Elaboration of the theory of families of sets. With the use of the universe $\D V_0$, of the notion of
a non-dependent assignment routine $\lambda_0$ from an index-set $I$ to $\D V_0$, and of a certain dependent operation $\lambda_1$, we
define explicitly in Definition <ref> the notion of a family of sets indexed by $I$.
Although an $I$-family of sets is a certain function-like object, it can be understood also as an object of
a one level higher than that of a set. 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. The constructions for families of sets can be generalised
appropriately for families of families of sets (see Section <ref>). 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 here and have many
applications in constructive mathematics.

Here we apply the general theory of families of sets, in order:

I. To reveal proof-relevance in $\BISH$. Classical mathematics is proof-irrelevant, as it is indifferent
to objects that “witness” a relation or a more complex formula. On the other extreme, Martin-Löf type theory
is proof-relevant, as every element of a type $A$ is a proof of the “proposition” $A$. Bishop's presentation
of $\BISH$ was on purpose closer to the proof-irrelevance of classical mathematics, although a form of proof-relevance
was evident in the use of several notions of moduli (of convergence, of uniform continuity, of uniform
differentiability etc.). Focusing on membership and equality conditions for sets given by appropriate existential
formulas we define certain families of proof-sets that provide a $\BHK$-interpretation within $\BST$ of formulas
that correspond to the standard atomic formulas of a first order theory. With the machinery of the general theory
of families of sets this $\BHK$-interpretation within $\BST$ is extended to complex formulas. Consequently, we can associate to many formulas $\phi$ of $\BISH$ a set $\Prf(\phi)$ of “proofs” or witnesses of $\phi$. Abstracting
from several examples of totalities in $\BISH$ we define the notion of a set with a proof-relevant equality,
and of a Martin-Löf set, a special case of the former, the equality of which corresponds to the identity type of
a type in intensional $\MLTT$. Through the concepts and results of $\BST$ notions and facts of $\MLTT$ and its
extensions (either with the axiom of function extensionality, or with Vooevodsky's axiom of univalence) can be
translated into $\BISH$. While Bishop's theory of sets is standardly understood through its translation to
$\MLTT$ (see e.g., [39]), the development of $\BST$ offers a (partial) translation in the converse

II. 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 real-valued function $\D F(X)$ on $X$ that includes the constant functions and it is closed
under addition, composition with Bishop continuous functions $\BR$ from $\Real $ to $\Real$, 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 in
Chapter <ref>, in analogy to the classical theory of spectra of topological spaces and their limits.
The constructive theory of spectra of other structures, like groups, or rings, or modules, can be developed
along the same lines.

III. To reformulate predicatively the basics of Bishop-Cheng measure theory. The standard approach
to measure theory (see e.g., [125], [57]) is to take measure as a primitive notion, and to
define integration with respect to a given measure. An important alternative, and, as argued by
Segal in [120] and [121], a more natural approach to measure theory,
is to take the integral on a certain set of functions as a primitive notion, extend its definition to an appropriate,
larger set of functions, and then define measure at a later stage. This is the idea of the Daniell integral,
defined by Daniell in [43],
which was taken further by Weil, Kolmogoroff, and Carathéodory (see [130], [67], and [29],

In the general framework of constructive-computable mathematics, there are many approaches
to measure and probability theory. There is an extended literature in intuitionistic measure theory
(see e.g., [59]), in measure theory within the computability framework of Type-2 Theory of Effectivity
(see e.g., [46]), in Russian constructivism (especially in the work of Šanin [114]
and Demuth [21]), in type theory, where the main interest lies in the creation of probabilistic programming
(see e.g., [8]), and recently also in homotopy type theory (see [47]), where
homotopy type theory (see [127]) is applied to probabilistic programming.

Within $\BISH$, measure and probability theory have taken two main directions.
The first direction, developed by Bishop and Cheng in [18] and by Chan in [30]$-$[34],
is based on the notion of integration space, a constructive version of the Daniell integral, as
a starting point of constructive measure theory. Following the aforementioned
spirit of classical algebraic integration theory, Bishop and Cheng defined first
the notion of an integrable function through the notion of an integration space, and afterwords
the measure of an integrable set. In their definition of integration space though, Bishop and Cheng used the
impredicative concept $\C F(X)$ of all partial functions from a set $X$ to $\Real$. Such a notion makes the
extraction of the computational content of $\CMT$ and the implementation of $\CMT$ in some programming language impossible.
The second direction to constructive measure theory, developed by Coquand, Palmgren and Spitters
in [38], [123] and [41], is based on the recognition of the above problem of the
Bishop-Cheng theory and of the advantages of working within the abstract, algebraic, and point-free framework of
Boolean rings or of vector lattices. In analogy to Segal's notion of a probability algebra, the starting notion
is a boolean ring equipped with
an inequality and a measure function, which is called a measure ring, on which integrable and measurable
functions can be defined. One can show that the integrable sets of Bishop-Cheng form a measure ring. In general,
the second direction to constructive measure theory is considered technically and conceptually simpler.

In Chapter <ref> we reconstruct the Bishop-Cheng notion of measure space within $\BST$, where a
set of measurable sets is not an appropriate set of complemented subsets, as it is usually understood, but an
set-indexed family of complemented subsets. This fact is acknowledged by Bishop in [12], but it is
completely suppressed later by him and his collaborators (Cheng and Chan). A similar indexing appears in a
predicative formulation of the Bishop-Cheng notion of an integration space.

The notions of a set-indexed family of sets and of a set-indexed family of subsets of a given set are shown here to be
important tools in the precise formulation of abstract notions in constructive mathematics. Avoiding them,
makes the reading of constructive mathematics easier and very close to the reading of classical mathematics.
Using them, makes the writing of constructive mathematics more precise, and seriously enriches its content.

As the fundamental notion of a family of sets can be described both in categorical and type-theoretic terms,
many notions and constructions from category theory and dependent type theory are represented in $\BST$.
While category theory and standard set-theory, or dependent type theory and standard set-theory do not match perfectly,
large parts of category theory and dependent type theory are reflected naturally in Bishop Set Theory (see also section <ref>).

§ NOTES

Regarding the exact time that Bishop's unpublished papers [10] and [11] were written,
it was difficult to find an answer. Bishop's scheme of presenting a formal system for $\BISH$ and of elaborating its implementation in some functional programming language is found both in [12] and in Bishop's unpublished papers.
The first is Bishop's contribution to the proceedings of the Buffalo meeting in 1968 that were
published in [66]. As Per Martin-Löf informed me, Bishop was not present at the meeting.
The presentation of the formal system $\Sigma$ and its presentation as a programming language in [12] is
very sketchy. Instead, the presentation of the type theory for $\BISH$ in [10], and its presentation as
a programming language in [11] is an elaborated enterprise. I have heard a story of an unsuccessful
effort of Bishop to publish [10], due to some parallels between [10] and de Bruijn's work.
According to that story, Bishop was unwilling to pursue the publication of his type-theoretic formalism after
that rejection. In any event, Bishop's unpublished papers must have been written between 1967 and 1970. Maybe,
the period between 1968 and 1969 is a better estimation. In October 1970 Bishop and Cheng sent to the editors
of the Memoirs of the American Mathematical Society their short monograph [18], a work that deviates a
lot from the predicative character of [9]. In my view, the papers [10] and [11] do not
fit to Bishop's period after 1970.

[The presentation axiom for setoids]
If $A : \C U$, then, by Martin-Löf's $J$-rule, $=_A$ is the least reflexive relation on $A$, and
$\varepsilon A := (A, =_A)$ is the free setoidfree setoid on $A$. According to the universal
property of a free setoid, for every setoid $\C B := (B, \sim_B)$ and every function $f : A \to B$, there is
a setoid-map $\varepsilon f \colon A \to \C B$ such that the following left diagram commutes

(E) at (0,0) $A$;
[above=of E] (F) $A$;
[right=of F] (A) $B$;
[right=of A] (K) $A$;
[right=of K] (L) $B$.;
[below=of K] (M) $P$;

[->,dashed] (E)–(A) node [midway,right] $ \ \varepsilon f$;
[->] (F)–(E) node [midway,left] $\id_A$;
[->] (F)–(A) node [midway,above] $f$;

[->,dashed] (M)–(K) node [midway,left] $h$;
[->>] (K)–(L) node [midway,above] $f$;
[->] (M)–(L) node [midway,right] $\ g$;

To show this, let $(\varepsilon f)(a) := f(a),$ and since $=_B$ is the least reflexive relation on $B$, we get
$a =_A a{'} \To (\varepsilon f)(a) =_B (\varepsilon f)(a{'})$, hence $f(a) \sim_B f(a{'})$.
A setoid $\C A$ is a choice setoid,choice setoid  if every $f: X \twoheadrightarrow A$, has a right
inverse i.e., there $g \colon A \to X$ such that $f \circ g = \id_A$.
With the use of the type-theoretic axiom of choice (see [127], section 1.6)  one can show that the free setoid
$(A, =_A)$ is a choice setoid. Using the identity map, every setoid $\C A$ is the quotient of the free setoid on $A$,
hence every setoid is the quotient of a choice setoid.
If $\C C$ is a category, an object $P$ of $\C C$ is called projective,projective object of a category
if for every objects $A, B$ of $\C C$ and every arrow $f : A \twoheadrightarrow B$ and $g \colon P \to B$,
there is $h \colon P \to A$ such that the above right diagram commutes.
A category
$\C C$ satisfies the presentation axiom,presentation axiom if for every object $C$ in $\C C$ there
is $f: P \twoheadrightarrow C$, where
$P$ is projective. For the relation between the presentation axiom and various choice principles
see [105].
It is immediate to show that a projective setoid is a choice setoid. For the converse, and following [39],
p. 74, let $(P, \sim_P)$ be a choice setoid. To show that  it is a projective, we need to define a setoid-map $h$,
given setoid maps $f$ and $g$ as above. Let

\[Q := \sum_{(a,p) : A \times P}f(a) =_B g(p),\]

and let the projections $p_1 : Q \to A,$, where $p_1(a,p,e) := a$,
and $p_2 \colon Q \to P$, where $p_2(a,p,e) := p$. By the definition of $Q$ we get $f \circ p_1 = g \circ p_2$.
Since $p_2 \colon Q \twoheadrightarrow P$ and $P$ is a choice set, there is $k \colon P \to Q$ such that
$p_2 \circ k = \id_P$. If $h := p_1 \circ k$, then

(E) at (0,0) $P$;
[above=of E] (F) $A$;
[right=of F] (A) $B$;
[left=of E] (B) $ \ Q$;
[left=of B] (C) $ \ P$;

[->>] (F)–(A) node [midway,above] $f$;
[->] (E)–(A) node [midway,right] $\ g$;
[->,bend left] (C) to node [midway,left] $h \ \ $ (F) ;

[->>] (B)–(E) node [midway,below] $p_2$;
[->] (B)–(F) node [midway,left] $p_1 \ $;
[->] (C)–(B) node [midway,below] $k$;

$f \circ (p_1 \circ k) = (f \circ p_1) \circ k = (g \circ p_2) \circ k = g \circ (p_2 \circ k) =
g \circ \id_P = g$. Consequently, every setoid is the surjective image of a choice setoid, hence of a projective setoid.

A very first and short presentation of $\BST$  is found in [95], where there we write
$\CSFT$ instead of $\BST$. In [95] we also expressed
dependency through the universe of functions $\D V_1$ i.e., the totality of triplets
$(A, B, f)$, where $A, B$ are sets and $f$ is a function from $A$ to $B$. Since dependent operations
are explicitly used by Bishop e.g., in the definition of the intersection $\bigcap_{t \in T}\lambda(t)$
of a $T$-family of subsets $(\lambda(t))_{t \in T}$ of a set $X$, while $\D V_1$ is neither explicitly, nor implicitly, mentioned, we
use here the former concept.

As it is noted by Palmgren in [82], p. 35, in $\ZF$, and also in its constructive version $\CZF$, a
family of sets is represented by the fibers of a function $\lambda \colon B \to I$, where the fibers
$\lambda_i := \{ b \in B \mid \lambda(b) = i\}$ of $\lambda$, for every $i \in I$, represent the sets of the
family. Hence the notion of a family of sets is reduced to that of a set. As this reduction rests on the
replacement scheme, such a reduction is not possible neither in $\MLTT$ nor in $\BST$.

CHAPTER: FUNDAMENTALS OF BISHOP SET THEORY

We present the basic elements of $\BST$, a reconstruction of Bishop's informal theory of sets, as this is
developed in chapters 3 of [9] and [19]. The main new features of $\BST$, with respect to Bishop's
account, are the explicit use of the universe $\D V_0$ of sets and the elaboration of the study of dependent
operations over a non-dependent assignment routines from a set to $\D V_0$. The first notion is implicit in Bishop's work,
while the second is explicitly mentioned, although in a rough way. These concepts are necessary to the concrete
definition of a set-indexed family of sets, the main object of our study, which is only roughly mentioned by Bishop.
The various notions of families of sets introduced later, depend on the various notions of sets, subsets and assignment
routines developed in this chapter.

§ PRIMITIVES

The logical framework of $\BST$ is first-order intuitionistic logic with equality (see [118], chapter 1).
This primitive equality between terms is
denoted by $s := t$$s := t$, and it is understood as a definitional, or logical,
equalitydefinitional equalitylogical 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)] \To \phi(b)$ we use the notation $[a := b \ \& \ \phi(a)] :\To \phi(b)$.
The equivalence notation $:\TOT$ is understood in the same way.
The set $(\Nat =_{\Nat}, \neq_{\Nat})$ of natural numbers, where its canonical equality is given by$=_{\Nat}$
$m =_{\Nat} n :\TOT m := n$, and its canonical inequality by $m \neq_{\Nat} n :\TOT \neg(m =_{\Nat} n)$, is primitive.
The standard Peano-axioms are associated to $\Nat$.

A global operation $( \cdot, \cdot)$ of pairingpairing 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{'}, t{'}) :\TOT s := s{'} \ \& \ t := t{'}$. The $n$-tuples of given terms, for every $n$ larger
than $2$, are definable. The global projection routines $\prb_1(s, t) := s$ and $\prb_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 primitive objects of $\BST$ are totalitiestotality and assignment
routinesassignment routine. Sets are special totalities and
functions are special assignment routines, where an assignment routine is a a special finite routine.
All other equalities in $\BST$ are equalities on totalities defined though an equality condition.
A predicatepredicate on a set on a set $X$ is a bounded formula $P(x)$ with $x$ a free variable ranging over $X$,
where a formula is boundedbounded formula, if every quantifier occurring in it is over a given set.

§ TOTALITIES

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

A $($non-inductive$)$defined totalitydefined totality $X$ is defined by a membership
condition $x \in X : \TOT \C M_X(x),$ where
$\C M_X$ is a formula with $x$ as a free variable.
If $X, Y$ are defined totalities with membership conditions $\C M_X $ and $\C M_Y$, respectively, we define
$X := Y : \TOT \big[\C M_X (x) : \TOT \C M_Y (x)\big]$, and in this case

we say that $X$ and $Y$ are definitionally equaldefinitionally equal defined totalities.

There is a special “open-ended” defined totality $\D V_0$, which is called the universe of sets. $\D 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 $\D 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 $\D V_0$.

A defined presetdefined preset $X$, or simply, a presetpreset, is a defined totality
$X$ the membership condition $\C M_X$ of which expresses a construction that can, in principle,
be carried out in a finite time. Formally this is expressed by the requirement
that no quantification over $\D V_0$ occurs in $\C M_X$.

A defined totality $X$ with equalitydefined totality with equality, or simply, a
totality $X$ with equalitytotality with equality is a defined totality $X$ equipped with an equality condition
$x =_X y : \TOT \C E_X(x, y)$, where $\C E_X(x,y)$ is a formula with free variables $x$ and $y$ that
satisfies the conditions of an equivalence relation i.e., $\C E_X(x, x)$ and
$\C E_X(x, y) \To \C E_X(y, x)$, and $[\C E_X(x, y) \ \& \ \C E_X(y, z)] \To \C E_X(x, y)$.
Two defined totalities with equality $(X,=_X)$ and $(Y, =_Y)$ are definitionally equal, if
$\C M_X (x) : \TOT \C M_Y (x)$ and $\C E_X (x, y) : \TOT \C E_Y (x,y)$.

A defined setdefined set is a preset with a given equality.

A setset is either a primitive set, or a defined set.

A totality is a classclass, if it is the universe $\D V_0$, or if
quantification over $\D V_0$ occurs in its membership condition.

If $X, Y$ are sets, their productproduct of sets $X \times Y$$X \times Y$ is the
defined totality
with equality

\[ (x, y) \in X \times Y : \TOT x \in A \ \& \ y \in B, \]

\[ z \in X \times Y :  \TOT \exists_{x \in A}\exists_{y \in B}\big(z := (x, y)\big). \]

$X \times Y$ is considered to be a set, and its membership condition is written simpler as follows:

\[ (x, y) =_{X \times Y} (x{'}, y{'}) : \TOT x =_X x{'} \ \& \ y =_Y y{'}. \]

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

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

The totality $X_P$$P_X$ generated by $P(x)$ is defined by $x \in X_P : \TOT x \in X \ \& \ P(x)$,

\[ x \in X_P : \TOT x \in X \ \& \ P(x), \]

and the equality

of $X_P$ is inherited from the equality

of $X$. We  also write $X_P := \{x \in X \mid P(x)\}$.

The totality $X_P$ is considered to be a set, and it is called the
extensional subsetextensional subset of $X$ generated by $P$.

Using the properties of an equivalence relation, it is immediate to show that an equality condition
$\C E_X(x,y)$ on a totality $X$ is an extensional property on the product $X \times X$ i.e.,
$[(x, y) =_{X \times Y} (x{'}, y{'}) \ \&\ x =_X y] \To x{'} =_X y{'}$. Let the following extensional subsets of
$\Nat$: $\D 1$ $\D 2$

\[ \D 1 := \{x \in \Nat \mid x =_{\Nat} 0\} := \{0\}, \]

\[ \D 2 := \{x \in \Nat \mid x =_{\Nat} 0 \ \vee x =_{\Nat} 1\} := \{0, 1\}. \]

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

If $(X, =_X)$ is a set, its diagonaldiagonal of a set

$D(X, =_X)$
is the extensional subset of $X \times X$

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

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

Let $X$ be a set. An inequalityinequality on $X$, or an
apartness relationapartness relation on $X$, is a relation $x \neq_X y$$x \neq_X y$ such that
the following conditions are satisfied:

$(\Ap_1)$ $\forall_{x, y \in X}\big(x =_X y \ \& \ x \neq_X y \To \bot \big)$.

$(\Ap_2)$ $\forall_{x, y \in X}\big(x \neq_X y \To y \neq_X x\big)$.

$(\Ap_3)$ $\forall_{x, y \in X}\big(x \neq_X y \To \forall_{z \in X}(z \neq_X x \ \vee \ z \neq_X y)\big)$.

We write $(X, =_X, \neq_X)$$(X, =_X, \neq_X)$ to denote the equality-inequality structure of a
setequality-inequality structure of a set $X$, and for simplicity we refer the set
$(X, =_X, \neq_X)$. The set $(X, =_X, \neq_X)$ is called discretediscrete, if

\[ \forall_{x, y \in X}\big(x =_X y \ \vee \ x \neq_X y\big). \]

An inequality $\neq_X$ on $X$ is called tighttight inequality,
if $\neg(x \neq_X y) \To x =_X y$, for every $x,y \in X$.

An inequality relation $x \neq_X y$ is extensional on $X \times X$.

We show that if $x, y \in X$ such that $x \neq y$, and if $x{'}, y{'} \in X$ such that $x{'} =_X x$
and $y{'} =_X y$, then
$x{'} \neq y{'}$. By $\Ap_3$ we have that $x{'} \neq x$, which is excluded from $\Ap_1$, or $x{'} \neq y$,
which has to be the case. Hence, $y{'} \neq x{'}$, or $y{'} \neq y$. Since the last option is excluded similarly,
we conclude that $y{'} \neq x{'}$, hence $x{'} \neq y{'}$.

If $\neq_X$ is an inequality on $X$, and $P(x)$ is an extensional property on $X$, then $X_P$
inherits the inequality from $X$. Since $n \neq_{\Nat} m :\TOT \neg(n =_{\Nat} m)$,
the sets $\Nat$, $\D 1$, and $\D 2 $ are discrete. Clearly, if $(X, =_X, \neq_X)$ is discrete, then $\neq_X$ is tight.

Let the sets $(X, =_X, \neq_X)$ and $(Y, =_Y, \neq_Y)$.

The canonical inequality on $X \times Y$canonical inequality on $X \times Y$ induced
by $\neq_X$ and $\neq_Y$, which is
defined by

\[ (x, y) \neq_{X \times Y} (x{'}, y{'}) :\TOT x \neq_X x{'} \ \vee \ y \neq_Y y{'}, \]

for every $(x,y)$ and $(x{'}, y{'}) \in X \times Y$, is an inequality on $X \times Y$.

If $(X, =_X, \neq_X)$ and $(Y, =_Y, \neq_Y)$ are discrete, then
$(X \times Y, =_{X \times Y}, \neq_{X \times Y})$ is discrete.

The proof of (i) is immediate. To show (ii), let $(x, y), (x{'}, y{'}) \in X \times Y$. By our
hypothesis $x =_X x{'} \ \vee \ x \neq_X x{'}$ and
$y =_Y y{'} \ \vee \ y \neq_Y y{'}$. If $x =_X x{'}$ and $y =_Y y{'}$, then $(x, y) =_{X \times Y} (x{'}, y{'})$.
In any other case we get $(x, y) \neq_{X \times Y} (x{'}, y{'})$.

Uniqueness of an element of a set $X$ with respect to some property $P(x)$ on $X$ means that all elements
of $X$ having this property are $=_X$-equal. We use the following abbreviation:

\[\exists_{!x \in X}P(x) :\TOT \exists_{x \in X}\big(P(x) \ \& \ \forall_{z \in X}\big(P(z) \To z =_X x\big)\big). \]

Let $(X, =_X)$ be a set.

$X$ is inhabitedinhabited set, if
$\exists_{x \in X}\big(x =_X x\big)$.

$X$ is a singletonsingleton, or contractiblecontractible, or
a $(-2)$-set$(-2)$-set, if
$\exists_{x_0 \in X}\forall_{x \in X}\big(x_0 =_\mathsmaller{X} x\big)$. In this case,
$x_0$ is called a centre of contractioncentre of contraction for $X$.

$X$ is a subsingletonsubsingleton, or a mere propositionmere proposition,
or a $(-1)$-set$(-1)$-set, if $\forall_{x, y \in X}\big(x =_\mathsmaller{X} y\big)$.

The truncationtruncation of $(X, =_X)$ is the
set$\mathsmaller{\mathsmaller{\lvert \lvert =_X \rvert \rvert}}$
$(X, \mathsmaller{\mathsmaller{\lvert \lvert =_X \rvert \rvert}})$, where

\[ x \ \mathsmaller{\mathsmaller{\lvert \lvert =_X \rvert \rvert}} \ y :\TOT x =_X x \ \& \ y =_X y. \]

We use the symbol $||X||$ to denote that the set $X$ is equipped with the truncated
equality $\mathsmaller{\mathsmaller{\lvert \lvert =_X \rvert \rvert}}$.$||X||$

Clearly, $ x \ \mathsmaller{\mathsmaller{\lvert \lvert =_X \rvert \rvert}} \ y$, for every $x, y \in X$, and
$(X, \mathsmaller{\mathsmaller{\lvert \lvert =_X \rvert \rvert}})$ is a subsingleton.

§ NON-DEPENDENT ASSIGNMENT ROUTINES

Let $X, Y$ be totalities. A non-dependent assignment routinenon-dependent assignment routine
$f$ from $X$ to
$Y$, in symbols $f \colon X \sto Y$$f \colon X \sto 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 \sto Y$, let

\[f := g : \TOT \forall_{x \in X}\big(f(x) := g(x)\big). \]

If $f := g$, we say that  $f$ and $g$ are definitionally equaldefinitionally equal functions.
If $(X, =_X)$ and $(Y, =_Y)$ are sets, an operationoperation from $X$ to $Y$ is a non-dependent assignment routine
from $X$ to $Y$, while a functionfunction from $X$ to $Y$, in symbols $f \colon X \to Y$$f \colon X \sto Y$,
is an operation from $X$ to $Y$ that respects equality i.e.,

\[\forall_{x, x{'} \in X}\big(x =_X x{'} \To f(x) =_Y f(x{'})\big). \]

If $f \colon X \sto Y$ is a function from $X$ to $Y$, we say
that $f$ is a function, without mentioning the expression “from $X$ to $Y$”.
A function $\fXY$ is an embeddingembedding, in symbols
$f \colon X \hookrightarrow Y$$f \colon X \hookrightarrow Y$, if

\[\forall_{x, x{'} \in X}\big( f(x) =_Y f(x{'}) \To x =_X x{'}). \]

Let the sets $(X, =_X, \neq_X)$ and $(Y, =_Y, \neq_Y)$. A function $f \colon X \to Y$ is strongly extensional,
strongly extensional function if

\[ \forall_{x, x{'} \in X}\big(f(x) \neq_Y f(x{'}) \To x \neq_X x{'}\big). \]

If $\simeq_X$ is another equality on $X$, we use a new symbol e.g., $X^*$, for the same totality $X$.
When we write $f \colon X^* \to Y$, then $f$ is a function from $X$, equipped with the equality
$\simeq_X$, to $Y$.

If $X$ is a set, the identity mapidentity map on a set $\id_X$$\id_X$ on $X$ is the operation
$\id_X \colon X \sto X$, defined by $\id_X (x) := x$, for every $x \in X$. Clearly, $\id_X$ is an embedding,
which is strongly extensional, if $\neq_X$ is a given inequality on $X$.
If $Y$ is also a set, the projection maps $\pr_X$ and
$\pr_Y$$\pr_Y$$\pr_X$ on $X$ and $Y$, respectively, are the operations
$\pr_X \colon X \times Y \sto X$ and $\pr_Y \colon X \times Y \sto Y$, where

\[ \pr_X (x, y) := \prb_1 (x, y) := x \ \ \& \ \ \pr_Y (x, y) := \prb_2 (x, y) := y; \ \ \ \ (x, y) \in X \times Y. \]

Clearly, the operations $\pr_X$ and $\pr_Y$ are functions, which are strongly extensional, if $\neq_X, \neq_Y$ are
inequalities on $X, Y$, and $\neq_{X \times Y}$ is the canonical inequality on $X \times Y$ induced from them.
After introducing the universe $\D V_0$ of sets in section <ref>, we shall define non-dependent
assignment routines from a set to a totality, like $\D V_0$, which is not considered to be a set.
In most of the cases the non-dependent assignment routines defined here have a set as a domain.There are cases though,
see e.g., Definitions <ref> <ref>, <ref>,
and <ref>, where
a non-dependent assignment routine is defined on a totality, before showing that this totality
is a set. We never define a non-dependent assignment routine from a class to a totality.

Let the operation $m^* \colon \Real \sto \D Q$, defined by $m^*(a) := q_m$, where a real number $a$
is a regular sequence of rational numbers $(q_n)_n$ (see [19], p. 18), and $q_m$ is the $m$-term of this sequence.
for some fixed $m$. The operation $m^*$ is an example of an operation, which is not a function, since unequal
real numbers, with respect to the definition of $=_{\Real}$ in [19], p. 18, may have equal $m$-terms in $\D Q$.
To define a function $\fXY$, first we define the operation $f \colon X \sto Y$, and afterwords
we prove that $f$ is a function (from $X$ to $Y$).

The compositioncomposition of operations $g \circ f$$g \circ f$ of the operations $f \colon X \sto Y$
and $g \colon Y \sto Z$ is the operation $g \circ f \colon X \sto Z$, defined by $(g \circ f)(x) := g(f(x))$, for every
$x \in X$. Clearly, $g \circ f$ is a function, if $f$ and $g$ are functions. If $h \colon Z \sto W$, notice the
following definitional equalities

\[ f \circ \id_X := f, \ \ \ \ \id_Y \circ f := f, \ \ \ \ h \circ (g \circ f) := (h \circ g) \circ f. \]

A diagram commutes always with respect to the equalities of the related sets.
E.g., the commutativity of the following diagram is the equality $e (f(x)) =_W g(h(x))$, for every $x \in X$.

(E) at (0,0) $Z$;
[right=of E] (F) $W$.;
[above=of F] (A) $Y$;
[above=of E] (D) $X$;

[->] (E)–(F) node [midway,below] $g$;
[->] (D)–(A) node [midway,above] $f $;
[->] (D)–(E) node [midway,left] $h$;
[->] (A)–(F) node [midway,right] $e$;

Let $X, Y$ be sets, and $\neq_Y$ an inequality on $Y$. The totality $\D O(X, Y)$$\D O(X, Y)$ of
operations from $X$ to $Y$
is equipped with the following canonical equality and inequality:

\[ f =_{\D O(X, Y)} g : \TOT \forall_{x \in X}\big(f(x) =_Y f(x)\big), \]

\[ f \neq_{\D O(X, Y)} g : \TOT \exists_{x \in X}\big(f(x) \neq_Y f(x)\big). \]

The totality $\D O(X, Y)$ is considered to be a set. The set $\D F(X, Y)$$\D F(X, Y)$ of functions
from $X$ to $Y$
is defined by separation on $\D O(X, Y)$ through the extensional property $P(f) :\TOT
\forall_{x, x{'} \in X}\big(x =_X x{'} \To f(x) =_Y f(x{'})\big)$. The equality $=_{\D F(X, Y)}$ and
the inequality $\neq_{\D F(X, Y)}$ are inherited from $=_{\D O(X, Y)}$ and $\neq_{\D O(X, Y)}$, respectively.

Let the sets $(X =_X)$ and $(Y, =_Y, \neq_Y)$. If $\fXY$, let
$x_1 \neq_X^f x_2 : \TOT f(x_1) \neq_Y f(x_2)$, for every $x_1, x_2 \in X$.

$x_1 \neq_X^f x_2$ is an inequality on $X$.

If $(Y, =_Y, \neq_Y)$ is discrete, then $(X =_X,  \neq_X^f)$ is discrete if and only if $f$ is an

If $\neq_Y$ is tight, then $\neq_X^f$ is tight if and only if $f$ is an embedding.

(i) Conditions $(\Ap_1)$-$(\Ap_3)$ for $\neq_X^f$ are reduced to conditions $(\Ap_1)$-$(\Ap_3)$ for $\neq_Y$.

(ii) If $(X =_X,  \neq_X^f)$ is discrete, let $f(x_1) =_X f(x_2)$, for some $x_1, x_2 \in X$. Since the possibility
$x_1 \neq_X^f x_2 : \TOT f(x_1) \neq_Y f(x_2)$ is impossible, we conclude that $x_1 =_X x_2$. If $f$ is an embedding,
and since $f(x_1) =_X f(x_2)$ or $f(x_1) \neq_Y f(x_2)$, either $x_1 =_X x_2$, or $x_1 \neq_X^f x_2$.

(iii) If $\neq_X^f$ is tight, and  $f(x_1) =_X f(x_2)$,

then $\neg(x_1 \neq_X^f x_2)$,
hence $x_1 =_X x_2$. If $f$ is an embedding and $\neg(x_1 \neq_X^f x_2) \TOT \neg\big(f(x_1) \neq_Y f(x_2)\big)$,
then $f(x_1) =_X f(x_2)$, and $x_1 =_X x_2$.

A function $f \colon X \to Y$ is called surjectivesurjective function, if
$\forall_{y \in Y}\exists_{x \in X}\big(f(x) =_Y y\big)$. A function $g \colon Y \to X$ is called a modulus of
surjectivity for $f$modulus of surjectivity, if the following diagram commutes

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

[->] (E)–(F) node [midway,above] $g$;
[->] (F)–(A) node [midway,above] $f$;
[->,bend right] (E) to node [midway,below] $\id_Y$ (A);

If $g$ is a modulus of surjectivity for $f$, we also say that $f$ is a retractionretraction
and $Y$ is a retractretract of $X$.
If $y \in Y$, the fiberfiber $\fib^f(y)$$\fib^f(y)$ of $f$ at $y$ is the following
extensional subset of $X$

\[ \fib^f(y) := \{x \in X \mid f(x) =_Y y \}. \]

A function $\fXY$ is contractiblecontractible function, if $\fib^f(y)$ is contractible, for every $y \in Y$.
If $\neq_Y$ is an inequality on $Y$,  the cofibercofiber $\cofib^f(y)$$\cofib^f(y)$ of $f$ at $y$
is the following extensional subset of $X$

\[ \cofib^f(y) := \{x \in X \mid f(x) \neq_Y y \}. \]

§ THE UNIVERSE OF SETS

The totality of all sets is the universe $\D V_0$ of setsuniverse of sets$\D V_0$,

equipped with the canonical equality

\[ X =_{\D V_0} Y :\TOT \exists_{f \in \D F(X,Y)}\exists_{g \in \D F(Y,X)}\big(g \circ f = \id_X \ \& \
f \circ g = \id_Y\big) \]

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

[->] (E)–(F) node [midway,above] $f$;
[->] (F)–(A) node [midway,above] $\ \ \ g$;
[->] (A)–(B) node [midway,below] $f$;
[->,bend right] (E) to node [midway,below] $\id_X$ (A) ;
[->,bend left] (F) to node [midway,above] $\id_Y$ (B) ;

In this case we write $(f, g) : X =_{\D V_0} Y$. If $X, Y \in \D V_0$ such that $X =_{\D V_0} Y$, we
define the set

\[ \Eq(X, Y) := \big\{(f, g) \in \D F(X, Y) \times \D F(Y, X) \mid (f, g) : X =_{\D V_0} Y\big\} \]

of all objects that “witness”, or “realise”, or prove the equality $X =_{\D V_0} Y$. The equality of
$\Eq(X, Y)$ is the canonical one i.e., $(f, g) =_{\Eq(X, Y)} (f{'}, g{'}) :\TOT f =_{\D F(X, Y)} f{'} \ \&
\ g =_{\D F(Y, X)}g{'}$. Notice that, in general, not all elements of $\Eq(X, Y)$ are equal. As in [127],
Example 3.1.9, if $X := Y := \D 2 := \{0, 1\}$, then $(\id_{\D 2}, \id_{\D 2}) \in \Eq(\D 2, \D 2)$, and if
$\sw_{\D 2} : \D 2 \to \D 2$ maps $0$ to $1$ and $1$ to $0$, then $(\sw_{\D 2}, \sw_{\D 2}) \in \Eq(\D 2, \D 2)$, while
$\sw_{\D 2} \neq \id_{\D 2}$.

It is expected that the proof-terms in $\Eq(X, Y)$ are compatible with the properties of the equivalence relation
$X =_{\D V_0} Y$. This means that we can define a distinguished proof-term
$\refl(X) \in \Eq(X, X)$ that proves the reflexivity of $X =_{\D V_0} Y$, an operation $^{-1}$, such that
if $(f, g) : X =_{\D V_0} Y$, then $(f, g)^{-1} : Y =_{\D V_0} X$, and an operation of
“composition” $\ast$ of proof-terms,
such that if $(f, g) : X =_{\D V_0} Y$ and $(h, k) : Y =_{\D V_0} Z$, then $(f, g) \ast (h, k) : X =_{\D V_0} Z$.

If $h \in \D F(Y, W)$ and $k \in \D F(W, Y)$, let

$$\refl(X) := \big(\id_X, \id_X\big) \ \ \& \ \ (f, g)^{-1} := (g, f) \ \ \& \ \
(f, g) \ast (h, k) := (h \circ f, g \circ k).$$

It is immediate to see that these operations satisfy the groupoid lawsgroupoid laws:

(i) $\refl (X) \ast (f, g) =_{\Eq(X, Y)} (f, g)$ and $(f, g) \ast \refl (Y) =_{\Eq(X, Y)} (f, g)$.

(ii) $(f, g) \ast (f, g)^{-1} =_{\Eq(X, X)} \refl (X)$ and $(f, g)^{-1} \ast (f, g) =_{\Eq(Y, Y)} \refl (Y)$.

(iii) $\big((f, g) \ast (h, k)\big) \ast (s, t) =_{\Eq(X, W)} (f, g) \ast \big((h, k) \ast (s, t)\big)$.

Moreover, the following compatibility conditioncompatibility condition is satisfied:

(iv) If $(f, g), (f{'}, g{'}) \in \Eq(X, Y)$ and $(h, k), (h{'}, k{'}) \in \Eq(Y, Z)$, then
if $(f, g) =_{\Eq(X, Y)} (f{'}, g{'})$ and $(h, k) =_{\Eq(Y, Z)} (h{'}, k{'})$, then
$(f, g) \ast (h, k) =_{\Eq(X, Z)} (f{'}, g{'}) \ast (h{'}, k{'})$.

Let $X, Y$ be sets, $f \in \D F(X, Y)$ and $g \in \D F(Y,X)$. If $(f, g) \colon X =_{\D V_0} Y$,
then the set $\fib^f(y)$ is contractible, for every $y \in Y$.

If $y \in Y$, then $g(y) \in \fib^f(y)$, as $f(g(y)) =_Y \id_Y(y) := y$.
If $x \in X$,

$x \in \fib^f(y) :\TOT f(x) =_Y y$, and
$x =_X g(f(x)) =_X g(y)$ i.e., $g(y)$ is a centre of contraction for $\fib^f(y)$.

Let $X, Y$ be sets. The evaluation mapevaluation map$\ev_{X,Y}$
$\ev_{X,Y} : \D F(X, Y) \times X
\sto Y$ is defined by $\ev_{X,Y} (f, x) := f(x)$, for every $f \in \D F(X, Y)$ and $x \in X$.

Let $X, Y, Z$ be sets.

The evaluation map $\ev_{X,Y}$ is a function from $\D F(X, Y) \times X$ to $Y$.

For every function $h : Z \times X \to Y$, there is a unique function $\hat{h} : Z \to \D F(X, Y)$
such that for every $z \in Z$ and $x \in X$
$\ev_{X,Y}\big(\hat h (z), x\big) =_Y h(z, x).$

(i) By definition $(f, x) =_{\D F(X, Y) \times X} (f{'}, x{'})$ if and only if $f =_{\D F(X, Y)} f{'}$ and $x =_X x{'}$.
$\ev_{X,Y}(f, x) := f(x) =_Y f{'}(x) =_Y f{'}(x{'}) := \ev_{X,Y}(f{'}, x{'})$.

(ii) For every $z \in Z$, we define the assignment routine $\hat h$ from $Z$ to $\D F(X, Y)$ by
$z \mapsto \hat h (z)$, where
$\hat h(z)$ is the assignment routine from $X$ to $Y$, defined by
$\hat h(z)(x) := h(z, x),$
for every $x \in X$. First we show that $\hat h (z)$ is a function from $X$ to $Y$; if $x =_X x{'}$,
then $(z, x) =_{Z \times X} (z, x{'})$, hence $\hat h(z)(x) := h(z, x) =_Y h(z, x{'}) := \hat h(z)(x{'}).$
Next we show that the assignment routine $\hat h$ is a function from $Z$ to $\D F(X, Y)$; if $z =_Z z{'}$,
then, if $x \in X$, and since then $(z, x) =_{Z \times X} (z{'}, x)$, we have that
$\hat h(z)(x) := h(z, x) =_Y h(z{'}, x) := \hat h(z{'})(x).$ Since $x \in X$ is arbitrary, we conclude
that $\hat h (z) =_{\D F(X, Y)} \hat h(z{'})$. Since
$\ev_{X,Y}\big(\hat h (z), x\big) := \hat h(z)(x)  := h(z, x),$
we get the strong from of the required equality $\ev_{X,Y} \circ (\hat h \times 1_X) := h$.
If $g : Z \to \D F(X, Y)$ satisfying the required equality,
and if $z \in Z$, then, for every $x \in X$ we have that
$g(z)(x) := \ev_{X,Y}\big(g(z), x\big) =_Y h(z, x) =_Y \ev_{X,Y}\big(\hat h (z), x\big) := \hat h(z)(x),$
hence $g(z) =_{\D F(X, Y)} \hat h(z)$.

§ DEPENDENT OPERATIONS

Let $I$ be a set and $\lambda_0 \colon I \sto \D V_0$$\lambda_0 \colon I \sto \D V_0$ a non-dependent assignment
routine from $I$ to $\D V_0$.
A dependent operationdependent operation $\Phi$ over $\lambda_0$, in symbols

\[ \Phi \colon \bigcurlywedge_{i \in I} \lambda_0 (i), \]

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$-componentcomponent of a dependent operation
of $\Phi$, and we also use the notation $\Phi_i := \Phi(i)$$\Phi(i)$$\Phi_i$.
An assignment routineassignment 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)$,
let $\Phi := \Psi :\TOT \forall_{i \in I}\big(\Phi_i := \Psi_i\big).$

If $\Phi := \Psi$, we say that $\Phi$ and $\Psi$ are definitionally equaldefinitionally
equal dependent operations.

Let the non-dependent assignment routines $\lambda_0 \colon I \sto \D V_0, \mu_0 \colon I \sto \D V_0,
\nu_0 \colon I \sto \D V_0$ and $\kappa_0 \colon I \sto \D V_0$. Let

$\D F(\lambda_0, \mu_0) \colon
I \sto \D V_0$ be defined by $\D F (\lambda_0, \mu_0)(i) := \D F(\lambda_0(i), \mu_0(i)$, for every $i \in I$. The
identity operationidentity operation $\Id_{\lambda_0}$$\Id_{\lambda_0}$ over $\lambda_0$ is the
dependent operation

\[ \Id_{\lambda_0} \colon \bigcurlywedge_{i \in I}\D F(\lambda_0(i), \mu_0(i)) \ \ \ \ \Id_{\lambda_0}(i) :=
\id_{\lambda_0(i)}; \ \ \ \ i \in I.\]

$\Psi \colon \bigcurlywedge_{i \in I}\D F(\mu_0(i), \nu_0(i))$ and
$\Phi \colon \bigcurlywedge_{i \in I}\D F(\lambda_0(i), \mu_0(i))$. Their
compositioncomposition of dependent operations $\Psi \circ \Phi$$\Psi \circ \Phi$
is defined by

\[ \Psi \circ \Phi \colon \bigcurlywedge_{i \in I}\D F(\lambda_0(i), \nu_0(i)) \ \ \ \
(\Psi \circ \Phi)_i := \Psi_i \circ \Phi_i; \ \ \ \ i \in I. \]

If $\Xi \colon \bigcurlywedge_{i \in I}\D F(\nu_0(i), \kappa_0(i))$, notice the
following definitional equalities

\[ \Phi \circ \Id_{\lambda_0} := \Phi, \ \ \ \ \Id_{\mu_0} \circ \Phi := \Phi, \ \ \ \ \Xi \circ (\Psi \circ \Phi)
:= (\Xi \circ \Psi) \circ \Phi. \]

If $I$ is a set and $\lambda_0 : I \sto \D V_0$, let
$\D A(I, \lambda_0)$$\D A(I, \lambda_0)$ be the totality of dependent operations over $\lambda_0$,
equipped with the
canonical equality:

\[ \Phi =_{\D A(I, \lambda_0)} \Psi :\TOT \forall_{i \in I}\big(\Phi_i =_{\lambda_0(i)} \Psi_i\big). \]

The totality $\D A(I, \lambda_0)$ is considered to be a set. If $\neq_{\lambda_0(i)}$ is an inequality on $\lambda_0(i)$,
for every $i \in I$, the canonical inequality $\neq_{\D A(I, \lambda_0)}$ on $\D A(I, \lambda_0)$ is defined by
$\Phi \neq_{\D A(I, \lambda_0)} \Psi :\TOT \exists_{i \in I}\big(\Phi_i \neq_{\lambda_0(i)} \Psi_i\big)$.

Clearly, $\Phi =_{\D A(I, \lambda_0)} \Psi$ is an equivalence relation, and
$\Phi \neq_{\D A(I, \lambda_0)} \Psi$ is an inequality relation. If $i \in I$, the
$i$-projection map$i$-projection map on $\D A(I, \lambda_0)$ is the operation
$\pr_i^{\lambda_0} \colon \D A(I, \lambda_0) \sto \lambda_0(i)$, defined by $\pr_i^{\lambda_0}(\Phi) := \Phi_i$,
for every $i \in I$.

The operation $\pr_i^{\lambda_0}$ is a function. If $\Phi \colon \bigcurlywedge_{i \in I}\D F(\lambda_0(i),
\mu_0(i))$, a modulus of
surjectivity for $\Phi$modulus of surjectivity for a dependent operation is a
dependent operation  $\Psi \colon \bigcurlywedge_{i \in I}\D F(\mu_0(i), \lambda_0(i)$ such that
$\Phi \circ \Psi =_{\D A(I,  \D F(\lambda_0, \lambda_0)} \Id_{\lambda_0}$. In this case, $\Psi_i$ is a modulus of
surjectivity for $\Phi$, for  every $i \in I$.
If $\fXY$, let $\fib^f \colon Y \sto \D V_0$ be defined by $y \mapsto \fib^f(y)$, for every $y \in Y$. If $f$ is
then by Definition <ref> every fiber $\fib^f(y)$ of $f$ is contractible. A modulus of centres of
contractionmodulus of centres of contraction for a contractible function $f$ is a dependent operation
$\centr^f \colon \bigcurlywedge_{y \in Y}\fib^f(y)$,

such that $\centr^f_y := \centr^f(y)$ is a centre of contraction for $f$.

§ SUBSETS

Let $X$ be a set. A subsetsubset of $X$ is a pair $(A, i_A^X)$$(A, i_A^X)$, where $A$ is a set and
$\i_A^X \colon A \hookrightarrow X$ is an embedding of $A$ into $X$.
If $(A, i_A^X)$ and $(B, i_B^X)$ are subsets of $X$, then $A$ is a subsetsubset of $B$, in symbols
$(A, i_A^X) \subseteq (B, i_B^X)$$(A, i_A^X) \subseteq (B, i_B^X)$, or simpler
$A \subseteq B$$A \subseteq B$,
if there is $f \colon A \to B$ such that the following diagram commutes

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

[below=of B] (A) $X$.;

[->] (E)–(F) node [midway,above] $f$;

[right hook->] (E)–(A) node [midway,left] $i_A^X \ $;
[left hook->] (F)–(A) node [midway,right] $\ i_B^X$;

In this case we use the notation $f \colon A \subseteq B$. Usually we write $A$ instead of $(A, i_A^X)$.
The totality of the subsets of $X$ is the powersetpowerset $\C P(X)$$\C P(X)$ of $X$,
and it is equipped with the equality

\[ (A, i_A^X) =_{\C P(X)} (B, i_B^X) :\TOT A \subseteq B \ \& \ B \subseteq A. \]

If $f \colon A \subseteq B$ and $g \colon B \subseteq A$, we write $(f, g) \colon A =_{\C P(X)} B$.

Since the membership condition for $\C P(X)$ requires quantification over $\D V_0$, the totality
$\C P(X)$ is a class. Clearly, $(X, \id_X) \subseteq X$. If $X_P$ is an extensional subset of $X$ (see Definition <ref>), then $(X_P, i_P^X) \subseteq X$, where $i_P^X \colon X_P \sto X$ is defined by $i_P^X(x) := x$, for every
$x \in X_P$.

If $A, B \subseteq X$, and $f, g : A \subseteq B$, then $f$ is an embedding,
and $f =_{\D F(A, B)} h$

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

[left hook->,bend left] (E) to node [midway,above] $f$ (F);
[left hook->,bend right] (E) to node [midway,below] $h$ (F);
[right hook->] (E)–(A) node [midway,left] $i_A^X \ $;
[left hook->] (F)–(A) node [midway,right] $ \ i_B^X$;

If $a, a{'} \in A$ such that $f(a) =_B f(a{'})$, then
$i_B^X(f(a)) =_X i_B^X(f(a{'})) \TOT i_A^X(a) =_X i_A^X (a{'})$, which implies $a =_A a{'}$. Moreover, if
$i_B^X(f(a)) =_X i_A^X(a) =_X i_B^X(h(a))$, then $f(a) = h(a)$.

The “internal” equality of subsets implies their “external” equality as sets  i.e.,
$(f, g) : A =_{\C P(X)} B \To (f, g) : A =_{\D V_0} B$. If
$a \in A$, then $i_A^X(g(f(a))) =_X i_B^X(f(a)) = i_A^X (a)$, hence $g(f(a)) =_A a$, and then
$g \circ f =_{\D F(A, A)} \id_A$. Similarly we get $f \circ g =_{\D F(B, B)} \id_B$.
Let the set

\[ \Eq(A, B) := \big\{(f, g) \in \D F(A, B) \times \D F(B, A) \mid f \colon A \subseteq B \ \& \ g
\colon B \subseteq A\big\}, \]

equipped with the canonical equality of pairs as in the case of $\Eq(X, Y)$.

Because of the Proposition <ref>,
the set $\Eq(A, B)$ is a subsingleton i.e.,

\[ (f, g) \colon A =_{\C P(X)} B \ \& \ (f{'}, g{'}) \colon A =_{\C P(X)} B \To (f, g) = (f{'}, g{'}). \]

If $f \in \D F(A, B), g \in \D F(B, A), h \in \D F(B, C)$, and $k \in \D F(C, B)$, let
$\refl(A) := \big(\id_A, \id_A\big)$ and $(f, g)^{-1} := (g, f)$, and $(f, g) \ast (h, k) := (h \circ f, g \circ k)$,

and the properties (i)-(iv) for $\Eq(A, B)$ hold by the equality of all their elements.

Let the set $(X, =_X, \neq_X)$ and $\big(A, =_A, i_A^X, \neq_{A}^{\mathsmaller{i_A^X}}\big) \subseteq X$,
where the canonical inequalitycanonical inequality on a subset $\neq_{A}^{\mathsmaller{i_A^X}}$ on $A$ is
given by
$a \neq_{A}^{\mathsmaller{i_A^X}} a{'} :\TOT i_A^X(a) \neq_X i_A^X(a{'})$, for every $a, a{'} \in A$.
If $(X, =_X, \neq_X)$ is discrete, then $\big(A, =_A, i_A^X, \neq_{A}^{\mathsmaller{i_A^X}}\big)$ is discrete,
and if $\neq_X$ is tight, $\neq_{A}^{\mathsmaller{i_A^X}}$ is tight.

Since $i_A^X$ is an embedding, it follows immediately from Remark <ref>.

If $P, Q$ are extensional properties on the set $X$, then

\[ X_P =_{\C P (X)} X_Q \TOT \forall_{x \in X}\big(P(x) \TOT Q(x)\big). \]

The implication $(\oT)$ is immediate to show, since the corresponding identity maps witness
the equality $X_P =_{\C P (X)} X_Q$.
For the converse implication, let $(f, g) : X_P =_{\C P (X)} X_Q$. Let $x \in X$ such that $P(x)$. By
the commutativity of the  following outer diagram

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

[left hook->,bend left] (E) to node [midway,above] $f$ (F);
[left hook->,bend left] (F) to node [midway,below] $g$ (E);
[right hook->] (E)–(A) node [midway,left] $i_P^X \ $;
[left hook->] (F)–(A) node [midway,right] $ \ i_Q^X$;

we get $ f(x) := i_Q^X(f(x)) =_X  i_P^X(x) := x$, and by the extensionality of
$Q$ and the fact that $Q(f(x))$ holds we get $Q(x)$. By the commutativity of the above inner diagram and the
extensionality of $P$ we get similarly the inverse implication.

If $(A, i_A^X), (B,i_B^X) \subseteq X$, their unionunion of subsets
$A \cup B$$A \cup B$

is the totality defined by

\[ z \in A \cup B : \TOT z \in A \ \vee \ z \in B, \]

equipped with the non-dependent assignment routine[Here we define a non-dependent assignment routine
on the totality $A \cup B$, without knowing beforehand that $A \cup B$ is a set. It turns out that $A \cup B$
is set, but for that we need to define $i_{A \cup B}^X$ first.]
$i_{A \cup B}^X : A \cup B \sto X$, defined by

\[ i_{A \cup B}^X(z) := \left\{ \begin{array}{lll}
i_A^X (z)    &\mbox{, $z \in A$}\\
{} \\
i_B^X (z)             &\mbox{, $z \in B$.}
\end{array}
\right.\]

If $z, w \in A \cup B$, we define $z =_{A \cup B} w :\Leftrightarrow i_{A \cup B}^X(z) =_X i_{A \cup B}^X(w).$

Clearly, $=_{A \cup B}$ is an equality on $A \cup B$, which is considered to be a set,

$i_{A \cup B}^X$ is an embedding of $A \cup B$ into $X$, and the pair
$\big(A \cup B, i_{A \cup B}^X\big)$ is a subset of $X$. Note that if $P, Q$ are extensional properties on $X$, then
$X_P \cup X_Q := X_{P \vee Q},$ since
$z \in X_{P \vee Q} : \TOT (P \vee Q)(z) : \TOT P(z) \ \mbox{or} \ Q(z) \TOT : z \in X_P \cup X_Q,$
and the inclusion map $i : X_P \cup X_Q \eto X$ is the identity, as it is for $X_{P \vee Q}$
(see Definition <ref>). If $\neq_X$ is a given inequality on $X$, the canonical inequality
on $A \cup B$ is determined in Corollary <ref>.

If $(A, i_A^X), (B,i_B^X) \subseteq X$, their intersectionintersection of subsets
$A \cap B$$A \cap B$ is the totality defined by separation on $A \times B$ as follows:

\[ A \cap B := \{(a, b) \in A \times B \mid i_A^X (a) =_X i_B^X (b)\}. \]

Let the non-dependent assignment routine $i_{A \cap B}^X : A \cap B \sto X$, defined by
$i_{A \cap B}^X(a, b) := i_A^X (a)$, for every $(a, b) \in A \cap B$.
If $(a, b)$ and $(a{'}, b{'})$ are in $A\cap B$, let

\[ (a, b) =_{A \cap B} (a{'}, b{'}) :\TOT i_{A \cap B}^X(a, b) =_X i_{A \cap B}^X(a{'}, b{'}) :\TOT
i_A^X (a) =_X i_A^X (a{'}). \]

We write $A \between B$$A \between B$ to denote that the intersection $A \cap B$ is inhabited.

Clearly, $=_{A \cap B}$ is an equality on $A \cap B$, which is considered to be a set,

$i_{A \cap B}^X$ is an embedding of $A \cap B$ into $X$, and

$\big(A \cap B, i_{A \cap B}^X\big)$ is a subset of $X$.
If $\neq_X$ is a given inequality on $X$, the canonical inequality on $A \cap B$ is determined in Corollary <ref>.
If $P, Q$ are extensional properties on $X$, then $X_P \cap X_Q$ has elements in
$X \times X$, while $X_{P \wedge Q}$ has elements in $X$, hence the two subsets are not definitionally equal.
Next we show that they are “externally” equal i.e., equal in $\D V_0$.

If $P, Q$ are extensional properties on the set $X$, then $X_{P \wedge Q} =_{\D V_0} X_P \cap X_Q$.

Since the inclusion maps corresponding to $X_P$ and $X_Q$ are the identities, let $f : X_{P \wedge Q}
\to X_P \cap X_Q$ with $f(z) := (z, z)$, for every $z \in X_{P \wedge Q}$, and let $g : X_P \cap X_Q
\to X_{P \wedge Q}$ with $g(a, b) := a$, for every $(a, b) \in X_P \cap X_Q$.  Hence, $f(g(a, b))
:= f(a) := (a, a)$, and since $(a, b) \in X_P \cap X_Q$, we have by definition that $P(a), Q(b)$
and $a =_X b$, hence $(a, a) =_{X \times X} (a, b)$. If $z \in X_{P \wedge Q}$, then $g(f(z)) := g(z, z) := z$.

Clearly, $X \cap X =_{\C P(X)} X$, while $\pr_A \colon (A \cap B, i_{A \cap B}^X) \subseteq (A, i_A)$ and the identity map
$e_A \colon A \to A \cup B$ witnesses the inequality $(A, i_A^X) \subseteq (A \cup B, i_{A \cup B}^X)$

(E) at (0,0) $A \cap B$;

[right=of E] (F) $A$;
[below=of F] (C) ;
[below=of C] (A) $X$;
[right=of F] (K) $A \cup B$;

[left hook->,bend left] (E) to node [midway,above] $\pr_A$ (F);
[right hook->] (F) to node [midway,left] $i_A^X$ (A);
[right hook->] (E)–(A) node [midway,left] $i_{A \cap B}^X \ $;
[left hook->] (K)–(A) node [midway,right] $ \ i_{A \cup B}^X$;
[left hook->,bend left] (F) to node [midway,above] $e_A$ (K);

The following properties of the union and intersection of subsets are easy to show.

Let $A, B$ and $C$ be subsets of the set $X$.

$A \cup B =_{\C P(X)} B \cup A$ and $A \cap B =_{\C P(X)} B \cap A$.

$A \cup (B \cup C) =_{\C P(X)} (A \cup B) \cup C$ and $A \cap (B \cap C) =_{\C P(X)} (A \cap B) \cap C$.

$A \cap (B \cup C) =_{\C P(X)} (A \cap B) \cup (A \cap C)$ and $A \cup (B \cap C) =_{\C P(X)}
(A \cup B) \cap (A \cup C)$.

Let $X, Y$ be sets, $(A, i_A^X) (C, i_C^X) \subseteq X$, $e \colon (A, i_A^X) \subseteq (C, i_C^X)$, $f \colon C \to Y$,
and $(B, i_B^Y) \subseteq Y$. The restrictionrestriction $f_{|_{A}}$$f_{|_{A}}$ of $f$
to $A$ is the function
$f_{_{A}} := f \circ e$

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

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

The image image $f(A)$$f(A)$ of $A$ under $f$ is the pair $f(A) := (A, f_{_{A}}),$
where $A$ is equipped with the equality
$a =_{f(A)} a{'} : \TOT f_{|_{A}}(a) =_Y f_{|_{A}}(a{'}),$
for every $a, a{'} \in A$. We denote
$\{f(a) \mid a \in A\} := f(A)$$\{f(a) \mid a \in A\}$.
The pre-image pre-image $f^{-1}(B)$$f^{-1}(B)$ of $B$ under $f$ is the set

\[ f^{-1}(B) := \{(c, b) \in C \times B \mid f(c) =_Y i_B^Y (b)\}. \]

Let $i_{\mathsmaller{f^{-1}(B)}}^C \colon f^{-1}(B) \eto C$, defined by
$i_{\mathsmaller{f^{-1}(B)}}^C(c, b) := c$, for every $(c,b) \in f^{-1}(B)$.
The equality of the extensional subset $f^{-1}(B)$ of $C \times B$ is
inherited from the equality of $C \times B$.

Clearly, the restriction $f_{|_{A}}$ of $\fXY$ to $(A, \i_A) \subseteq X$ is the function
$f_{_{A}} := f \circ i_A^X$. It is immediate to show that $f(A) \subseteq Y$ and $f^{-1}(B) \subseteq C$.
Notice that

\[ (A, i_A^X) =_{\C P(X)} (B, i_B^X) \To i_A^X (A) =_{\C P(X)} i_B^X (B), \]

since, if $(f, g) : (A, i_A^X) =_{\C P(X)} (B, i_B^X)$, then $i_A^X (a) =_X i_B^X (f(a))$ and $i_B^X (b)
=_X i_A^X (g(b))$, for every $a \in A$ and $b \in B$, respectively.
If $\neq_Y$ is a given inequality on $Y$, the canonical inequality on $f(A)$ is determined in
Corollary <ref>. Similarly, if $\neq_X$ is an inequality on $X$, $f \colon X \to Y$,
and $(B, i_B^Y) \subseteq Y$, the canonical inequality on $f^{-1}(B)$ is given by
$(x, b) \neq_{f^{-1}(B)} (x{'}, b{'}) :\TOT x \neq_X x{'}$, and not by the canonical inequality on $X \times B$.

Let $X, Y$ be sets, $A, B$ subsets of $X$, $C, D$ subsets of $Y$, and $f : X \to Y$.

$f^{-1}(C \cup D) =_{\C P(X)} f^{-1}(C) \cup f^{-1}(D)$.

$f^{-1}(C \cap D) =_{\C P(X)} f^{-1}(C) \cap f^{-1}(D)$.

$f(A \cup B) =_{\C P(Y)} f(A) \cup f(B)$.

$f(A \cap B) =_{\C P(Y)} f(A) \cap f(B)$.

$A \subseteq f^{-1}(f(A))$.

$f(f^{-1}(C) \cap A) =_{\C P(Y)} C \cap f(A)$, and $f(f^{-1}(C)) =_{\C P(Y)} C \cap f(X)$.

$(A, i_A^X), (B, i_B^X), (A{'}, i_{A{'}}^X) , (B, i_{B{'}}^X) \subseteq X$, such that
$A =_{\C P(X)} A{'}$ and $B =_{\C P(X)} B{'}$. Let also $(C, i_C^Y), (C{'}, i_{C{'}}^Y), (D, i_D^Y) \subseteq Y$, such that
$C =_{\C P(Y)} C{'}$, and let $\fXY$.

$A \cap B =_{\C P(X)} A{'} \cap B{'}$, and $A \cup B =_{\C P(X)} A{'} \cup B{'}$.

$f(A) =_{\C P(Y)} f(A{'})$, and $f^{-1}(C) =_{\C P(X)} f^{-1}(C{'})$.

$(A \times C, i_A^X \times i_C^Y) \subseteq X \times Y$,
where the map $i_A^X \times i_C^Y \colon A \times C \hookrightarrow X \times Y$ is defined by

\[ (i_A^X \times i_C^Y)(a, c) := \big(i_A^X(a), i_C^Y(c)\big); \ \ \ \ (a, c) \in A \times C. \]

$A \times C =_{\C P(X \times Y)} A{'} \times C{'}$.

$A \times (C \cup D) =_{\C P(X \times Y)} (A \times C) \cup (A \times D)$.

$A \times (C \cap D) =_{\C P(X \times Y)} (A \times C) \cap (A \cap D)$.

All cases are straightforward to show.

§ PARTIAL FUNCTIONS

Let $X, Y$ be sets. A partial functionpartial function from $X$ to $Y$ is a triplet
$(A, i_A^X, f_A^Y)$$(A, i_A^X, f_A^Y)$, where $(A, i_A^X) \subseteq X$, and $f_A^Y \in \D F(A, Y)$.
Often, we use only the symbol $f_A^Y$ instead of the triplet $(A, i_A^X, f_A^Y)$, and we also write
$f_A^Y \colon X \pto Y$. If $(A, i_A^X, f_A^Y)$ and $(B, i_B^X, f_B^Y)$ are partial functions from $X$ to $Y$,
we call $f_A^Y$ a subfunctionsufunction of $f_B^Y$, in symbols
$(A, i_A^X, f_A^Y) \leq (B, i_B^X, f_B^Y)$$(A, i_A^X, f_A^Y) \leq (B, i_B^X, f_B^Y)$, or simpler
$f_A^Y \leq f_B^Y$$f_A^Y \leq f_B^Y$,
if there is $e_{AB} \colon A \to B$ such that the following inner diagrams commute

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

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

[->] (E)–(F) node [midway,above] $e_{AB}$;
[->,bend right=40] (E) to node [midway,left] $f_A^Y$ (C);
[->,bend left=40] (F) to node [midway,right] $f_B^Y$ (C);
[right hook->] (E)–(A) node [midway,left] $i_A^X \ $;
[left hook->] (F)–(A) node [midway,right] $\ i_B^X  $;

In this case we use the notation $e_{AB} \colon f_A^Y \leq f_B^Y$.
The totality of partial functions from $X$ to $Y$ is the partial function space
partial function space$\C F(X,Y)$$\C F(X,Y)$,
and it is equipped with the equality

\[ (A, i_A^X, f_A^Y) =_{\C F(X,Y)} (B, i_B^X, f_B^Y) :\TOT f_A^Y \leq f_B^Y \ \& \ f_B^Y \leq f_A^Y. \]

If $e_{AB} \colon f_A^Y \leq f_B^Y$ and $e_{BA} \colon f_B^Y \leq f_A^Y$, we write $(e_{AB}, e_{BA}) : f_A^Y
=_{\C F(X,Y)} f_B^Y$.

Since the membership condition for $\C F(X,Y)$ requires quantification over $\D V_0$, the totality
$\C F(X,Y)$ is a class. Clearly, if $\fXY$, then $(X, \id_X, f) \in \C F(X,Y)$.
If $(e_{AB}, e_{BA}) : f_A^Y =_{\C F(X,Y)} f_B^Y$, then $(e_{AB}, e_{BA}) : A =_{\C P(X)} B$, and
$(e_{AB}, e_{BA}) : A =_{\D V_0} B$.
Let the set

\[ \Eq(f_A^Y, f_B^Y) := \big\{(f, g) \in \D F(A, B) \times \D F(B, A) \mid f \colon f_A^Y \leq f_B^Y
\ \& \ g \colon f_B^Y \leq f_A^Y\big\}, \]

equipped with the canonical equality of the product.

All the elements of $\Eq(f_A^Y, f_B^Y)$ are equal to each other.
If  $f \in \D F(A, B), g \in \D F(B, A), h \in \D F(B, C)$, and $k \in \D F(C, B)$, let

\[ \refl(f_A^Y) := \big(\id_A, \id_A\big) \ \ \& \ \ (f, g)^{-1} := (g, f) \ \ \& \ \
(f, g) \ast (h, k) := (h \circ f, g \circ k), \]

and the groupoid-properties for $\Eq(f_A^Y, f_B^Y)$ hold by the equality of its elements.

Let $(A, i_A^X, f_A^Y) \in \C F(X, Y)$ and $(B, i_B^Y, g_B^Z) \in \C F(Y, Z)$. Their compositioncomposition
of partial functions$g_B^Z \pcirc f_A^Y$

\[ g_B^Z \mathsmaller{\pcirc} f_A^Y := \bigg(\big(f_A^Y\big)^{-1}(B), \ i_A^X \circ e_{\mathsmaller{(f_A^Y)^{-1}(B)}}^A,
\ \big(g_B^Z \circ f_A^Y\big)^Z_{\mathsmaller{(f_A^Y)^{-1}(B)}}\bigg), \ \ \ \mbox{where}
\]

\[ \big(f_A^Y\big)^{-1}(B) := \big\{(a, b) \in A \times B \mid f_A^Y(a) =_Y i_B^Y(b)\big\}, \]

\[  e_{\mathsmaller{(f_A^Y)^{-1}(B)}}^A \colon \big(f_A^Y\big)^{-1}(B) \eto A, \ \ \ \ (a, b) \mapsto a; \ \ \ \ (a,b)
\in \big(f_A^Y\big)^{-1}(B), \]

\[ \big(g_B^Z \circ f_A^Y\big)^Z_{\mathsmaller{(f_A^Y)^{-1}(B)}}(a, b) := g_B^Z(b); \ \ \ \  (a,b)
\in \big(f_A^Y\big)^{-1}(B), \]

is a partial function that belongs to $\C F(X, Z)$. If $(A, i_A^X, i_A^X) \in \C F(X, X), (B, i_B^Y, i_B^Y) \in \C F(Y, Y)$, and
$(C, i_C^Z, h_C^W) \in \C F(Z, W)$, the following properties hold:

$f_A^Y \pcirc i_A^X =_{\C F(X,Y)} f_A^Y$ and $i_B^Y \pcirc f_A^Y =_{\C F(X,Y)} f_A^Y$.

$\big(h_C^W \pcirc g_B^Z\big) \pcirc f_A^X =_{\C F(X,Z)} h_C^W \pcirc \big(g_B^Z \pcirc f_A^X\big)$.

(i) We show only the first equality and for the second we work similarly. By definition

\[ f_A^Y \mathsmaller{\pcirc} i_A^X := \bigg(\big(i_A^X\big)^{-1}(A), \ i_A^X \circ e_{\mathsmaller{(i_A^X)^{-1}(A)}}^A,
\ \big(f_A^Y \circ i_A^X\big)^Y_{\mathsmaller{(i_A^X)^{-1}(A)}}\bigg), \ \ \ \mbox{where}
\]

\[ \big(i_A^X\big)^{-1}(A) := \big\{(a, a{'}) \in A \times A \mid i_A^X(a) =_X i_A^X(a{'})\big\}, \]

\[  e_{\mathsmaller{(i_A^X)^{-1}(A)}}^A \colon \big(i_A^X\big)^{-1}(A) \eto A, \ \ \ \ (a, a{'}) \mapsto a; \ \ \ \ (a,a{'})
\in \big(i_A^X\big)^{-1}(A), \]

\[ \big(f_A^Y \circ i_A^X\big)(a, a{'}) := f_A^Y(a{'}); \ \ \ \  (a,a{'}) \in \big(i_A^X\big)^{-1}(A). \]

Let the operations $\phi \colon A \sto \big(i_A^X\big)^{-1}(A)$, defined by $\phi(a) := (a, a)$, for every $a \in A$,
and $\theta \colon \big(i_A^X\big)^{-1}(A) \sto A$, defined by $\theta(a, a{'}) := a$, for every $(a, a{'}) \in
\big(i_A^X\big)^{-1}(A)$. It is immediate to show that $\phi$ and $\theta$ are well-defined functions. It is
straightforward to show the commutativity of the following inner diagrams

(E) at (0,0) $A$;
[right=of E] (B) ;
[right=of B] (F) $\big(i_A^X\big)^{-1}(A)$;

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

[->,bend left] (E) to node [midway,below] $\phi$ (F);
[->,bend left] (F) to node [midway,above] $\theta$ (E);
[->,bend right=50] (E) to node [midway,left] $f_A^Y$ (C);
[->,bend left=50] (F) to node [midway,right] $f_A^Y \circ i_A^X$ (C);
[right hook->,bend right=20] (E) to node [midway,left] $ \ i_A^X \ $ (A);
[left hook->,bend left=20] (F) to node [midway,right] $\ \ i_A^X \circ e_{\mathsmaller{(i_A^X)^{-1}(A)}}^A \ $ (A);

(ii) We have that
$ h_C^W \mathsmaller{\pcirc} g_B^Z := \bigg(\big(g_B^Z\big)^{-1}(C), \ i_B^Y \circ e_{\mathsmaller{(g_B^Z)^{-1}(C)}}^B,
\ \big(h_C^W \pcirc g_B^Z\big)^W_{\mathsmaller{(g_B^Z)^{-1}(C)}}\bigg)$, where

\[ \big(g_B^Z\big)^{-1}(C) := \big\{(b, c) \in B \times C \mid g_B^Z(b) =_Z i_C^Z(c)\big\}, \]

\[  e_{\mathsmaller{(g_B^Z)^{-1}(C)}}^B \colon \big(g_B^Z\big)^{-1}(C) \eto B, \ \ \ \ (b, c) \mapsto b; \ \ \ \ (b,c)
\in \big(g_B^Z\big)^{-1}(C), \]

\[ \big(h_C^W \circ g_B^Z\big)(b, c) := h_C^W(c); \ \ \ \  (b,c) \in \big(g_B^Z\big)^{-1}(C). \]

$\big(h_C^W \mathsmaller{\pcirc} g_B^Z\big) \mathsmaller{\pcirc} f_A^X := \bigg(D, i_A^X \circ e_D^A,
\big[\big(h_C^W \circ g_B^Z\big) \circ f_Z^X\big]_D^W\bigg)$, where

\[
D :=  \big(f_A^Y\big)^{-1}\big[\big(g_B^Z\big)^{-1}(C)\big]
:= \bigg\{(a, d) \in A \times \big[\big(g_B^Z\big)^{-1}(C)\big] \mid f_A^Y(a) =_Y \big(i_B^Y \circ
e_{\mathsmaller{(g_B^Z)^{-1}(C)}}^B\big)(d) \bigg\},
\]

with $d:= (b,c) \in B \times C$ such that $g_B^Z(b) =_Z i_C^Z(c)$. The map $e_D^A \colon D \eto A$ is defined by
the rule $(a, d) \mapsto a$, for every $(a,d) \in D$, and

\[ \big[\big(h_C^W \circ g_B^Z\big) \circ f_A^Y\big](a, d) := \big(h_C^W \circ g_B^Z\big)(d) := h_C^W(c); \ \ \ \
(a,d) := (a, (b,c)) \in D. \]

$h_C^W \mathsmaller{\pcirc} \big(g_B^Z \mathsmaller{\pcirc} f_A^Y\big) := \bigg(E, \
i_A^X \circ e_{(f_A^Y)^{-1}(B)}^A \circ e_E^{\mathsmaller{(f_A^Y)^{-1}(B)}}, \
\big[h_C^W \circ \big(g_B^Z \circ f_Z^X\big)\big]_E^W\bigg)$, where

\[ E :=  \bigg[\big(g_B^Z \circ f_A^Y\big)_{\mathsmaller{(f_A^Y)^{-1}(B)}}^Z\bigg]^{-1}(C)
:= \bigg\{(u, c) \in \big[\big(f_A^Y\big)^{-1}(B)\big] \times C \mid (g_B^Z \circ f_A^Y)(u) =_Z i_C^Z(c) \bigg\},
\]

$e_E^{\mathsmaller{(f_A^Y)^{-1}(B)}} \colon E \eto \big((f_A^Y\big))^{-1}(B)$ is defined by the rule
$(u, c) \mapsto u$, for every $(u,c) \in E$, and

\[ \big[h_C^W \circ \big(g_B^Z \circ f_A^Y\big)\big](u, c) := h_C^W(c); \ \ \ \
(u,c) \in E. \]

Let the operations $\phi \colon D \sto E$, defined by $\phi(a, (b,c)) := ((a,b), c)$, for every $(a, (b,c)) \in D$,
and $\theta \colon E \sto D$, defined by $\theta((a,b),c) := (a, (b,c))$, for every $((a,b),c) \in
E$. It is straightforward to show that $\phi$ and $\theta$ are well-defined functions, and that the
following inner diagrams commute

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

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

[->,bend left] (E) to node [midway,below] $\phi$ (F);
[->,bend left] (F) to node [midway,above] $\theta$ (E);
[->,bend right=80] (E) to node [midway,left] $\big(h_C^W \circ g_B^Z\big) \circ f_A^Y$ (C);
[->,bend left=80] (F) to node [midway,right] $h_C^W \circ \big(g_B^Z \circ f_A^Y\big)$ (C);
[right hook->,bend right=20] (E) to node [midway,left] $ \ \mathsmaller{i_A^X \circ e_D^A} \ $ (A);
[left hook->,bend left=20] (F) to node [midway,right] $\ \mathsmaller{i_A^X \circ e_{(f_A^Y)^{-1}(B)}^A
\circ e_E^{\mathsmaller{(f_A^Y)^{-1}(B)}}} \ $ (A);

The next proposition is straightforward to show.

Let $(A, i_A^X, f_A^Y), (B, i_B^X, f_B^X) \in \C F(X, Y)$

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

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

[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^Y \ \ $;
[->] (F)–(C) node [midway,right] $ \ f_B^Y$;

Their left $f_A^Y \cap_l f_B^Y$ and right
intersectionleft intersection of partial functions$f_A^Y \cap_l f_B^Y$
$f_A^Y \cap_r f_B^Y$ are the partial functionsright intersection of partial functions$f_A^Y \cap_r f_B^Y$

\[ f_A^Y \cap_l f_B^Y := \bigg(A \cap B, \ i_{A \cap B}^X, \ \big(f_A^Y \cap_l f_B^Y\big)_{A \cap B}^Y\bigg), \ \ \ \mbox{where}
\]

\[ \big(f_A^Y \cap_l f_B^Y\big)_{A \cap B}^Y(a, b) := f_A^Y(a); \ \ \ \  (a,b) \in A \cap B, \ \ \ \ \mbox{and} \]

\[ f_A^Y \cap_r f_B^Y := \bigg(A \cap B, \ i_{A \cap B}^X, \ \big(f_A^Y \cap_r f_B^Y\big)_{A \cap B}^Y\bigg), \ \ \ \mbox{where}
\]

\[ \big(f_A^Y \cap_r f_B^Y\big)_{A \cap B}^Y(a, b) := f_B^Y(b); \ \ \ \  (a,b) \in A \cap B. \]

Their union $f_A^Y \cup f_B^Y$union of partial functions$f_A^Y \cup f_B^Y$ is the partial function

\[ f_A^Y \cup f_B^Y := \bigg(A \cup B, \ i_{A \cup B}^X, \ \big(f_A^Y \cup f_B^Y\big)_{A \cup B}^Y\bigg), \ \ \ \mbox{where}
\]

\[ \big(f_A^Y \cup f_B^Y\big)_{A \cup B}^Y(z) := \left\{ \begin{array}{ll}
f_A^Y(z)   &\mbox{, $z \in A$}\\
f_B^Y(z)            &\mbox{, $z \in B$.}
\end{array}
\right.
\]

$f_A^Y \cap_l f_B^Y \leq f_A^Y$ and $f_A^Y \cap_r f_B^Y \leq f_B^Y$.

If $f_A^Y(a) =_Y f_B^Y(b)$, for every $(a,b) \in A \cap B$, then $f_A^Y \cap_l f_B^Y =_{\C F(X,Y)}
f_A^Y \cap_r f_B^Y$.

$f_A^Y \leq f_A^Y \cup f_B^Y$ and $f_B^Y \leq f_A^Y \cup f_B^Y$.

$f_A^Y \cup f_B^Y =_{\C F(X,Y)} f_B^Y \cup f_A^Y$.

Let the operation of multiplication on $\D 2$, defined by $0 \cdot 1 := 1 \cdot 0 := 0 \cdot 0 := 0$ and $1 \cdot 1 := 1$.
If $(A, i_A^X, f_A^{\D 2}), (B, i_B^X, g_B^{\D 2}) \in \C F(X, \D 2)$, let

\[ f_A \cdot g_B := \big(A \cap B, i_{A \cap B}^X, (f_A \cdot g_B)_{A \cap B}^{\D 2}\big), \]

where $(f_A \cdot g_B)_{A \cap B}^{\D 2} \colon A \cap B \to \D 2$ is defined, for every $(a, b) \in A \cap B$,
by$f_A \cdot g_B$

\[ (f_A \cdot g_B)_{A \cap B}^{\D 2}(a, b) := f_A^{\D 2}(a) \cdot g_B^{\D 2}(b). \]

By the equality of the product on $A \cap B$, it is immediate to show that the operation
$(f_A \cdot g_B)_{A \cap B}^{\D 2}$ is a function. More generally, operations on $Y$ induce
operations on $\C F(X, Y)$. The above example with $Y := \D 2$ is useful to the next section.

§ COMPLEMENTED SUBSETS

An inequality on a set $X$ induces a positively defined notion of disjointness of subsets of $X$.

Let $(X, =_X, \neq_X)$ be a set, and $(A, i_A^X), (B, i_B^X) \subseteq X$. We say that
$A$ and $B$ are disjoint with respect to $\neq_X$disjoint subsets, in symbols
$A \Disj_{\mathsmaller{\neq_X}} B$$A \Disj_{\mathsmaller{\neq}} B$, if

\[ A \underset{\mathsmaller{\mathsmaller{\mathsmaller{\neq_X}}}} \Disj B :
\TOT \forall_{a \in A}\forall_{b \in B}\big(i_A^X(a) \neq_X i_B^X(b) \big). \]

If $\neq_X$ is clear from the context, we only write $A \Disj B$$A \Disj B$.

Clearly, if $A \Disj B$, then $A \cap B$ is not inhabited.

The positive disjointness of subsets of $X$ induces the notion of a complemented subset of $X$, and
the negative notion of the complement of a set is avoided. We use bold letters to denote a complemented subset of a set.

A complemented subsetcomplemented subset of a set $(X, =_X, \neq_X)$ is a pair
$\B A := (A^1, A^0)$$\B A := (A^1, A^0)$,
where $(A^1, i_{A^1}^X)$ and $(A^0, i_{A^0}^X)$ are subsets of $X$ such that $A^1 \Disj A^0$. We
call $A^1$ the $1$-component of $\B A$$1$-component of a complemented subset and $A^0$ the
$0$-component of $\B A$$0$-component of a complemented subset. If
$\Dm(\B A) := A^1 \cup A^0$$\Dm(\B A)$ is the domain of $\B A$domain of a complemented subset,
indicator functionindicator function of a complemented subset, or
characteristic functioncharacteristic function of a complemented subset, of
$\B A$ is the operation $\chi_{\B A} : \Dm(\B A) \sto \D 2$ defined by

\[ \chi_{\B A}(x) := \left\{ \begin{array}{ll}
1   &\mbox{, $x \in A^1$}\\
0             &\mbox{, $x \in A^0$.}
\end{array}
\right. \]

Let $x \in \B A :\TOT x \in A^1$ and $x \notin \B A :\TOT x \in A^0$. If $\B A, \B B$ are complemented subsets of $X$, let

\[ \B A \subseteq \B B : \TOT A^1 \subseteq B^1 \ \& \ B^0 \subseteq A^0.  \]

Let $\C P^{\Disj}(X)$$\C P^{\Disj}(X)$$\B A \subseteq \B B$ be their totality,
equipped with the equality
$\B A =_{\C P^{\mathsmaller{\Disj}} (X)} \B B : \TOT \B A \subseteq \B B \ \& \ \B B \subseteq \B A$.

Let $\Eq(\B A, \B B) := \Eq(A^1, B^1) \times \Eq(A^0, B^0)$. A map $\B f \colon \B A \to \B B$ from $\B A$
to $\B B$ is a pair $(f^1, f^0)$, where $f^1 \colon A^1 \to B^1$ and
$f^0 \colon A^0 \to B^0$map between complemented subsets.

Clearly, $ \B A =_{\C P^{\mathsmaller{\Disj}} (X)} \B B \TOT A^1 =_{\C P(X)} B^1 \ \& \ A^0 =_{\C P(X)} B^0$,
and $\Eq(\B A, \B B)$ is a subsingleton, as the product of subsingletons.
Since the membership condition for  $\C P^{\mathsmaller{\Disj}} (X)$ requires quantification over $\D V_0$, the
totality  $\C P^{\mathsmaller{\Disj}} (X)$ is a class. The operation
$\chi_{\B A}$ is a function, actually, $\chi_{\B A}$ is a partial function in $\C F(X, \D 2)$.
Let $z, w \in A^1 \cup A^0$ such that $z =_{A^1 \cup A^0} w$ i.e.,

\[  \left.
\begin{array}{lll}
i_{A^1}^X(z)   &\mbox{, $z \in A^1$}\\
i_{A^0}^X(z)             &\mbox{, $z \in A^0$}
\end{array}
\right\}
:= i_{A^1 \cup A^0}^X(z)
i_{A^1 \cup A^0}^X(w) := \left\{ \begin{array}{lll}
i_{A^1}^X(w)   &\mbox{, $w \in A^1$}\\
i_{A^0}^X(w)           &\mbox{, $w \in A^0$.}
\end{array}
\right.
\]

Let $z \in A^1$. If $w \in A^0$, then $i_{A^1}^X(z) := i_{A^1 \cup A^0}^X(z) =_X i_{A^1 \cup A^0}^X(w) := i_{A^0}^X(w)$
i.e., $(z, w) \in A^1 \cap A^0$, which contradicts the hypothesis $A^1 \Disj A^0$. Hence $w \in A^1$, and
$\chi_{\B A}(z) = \chi_{\B A}(w)$. If $z \in A^0$, we proceed similarly.

If $(X, =_X)$ is a set, let the inequality on $X$ defined by

\[ x \neq_X^{\mathsmaller{\D F(X, \D 2)}} x{'} : \TOT \exists_{f \in \D F(X, \D 2)}\big(f(x)
=_{\mathsmaller{\D 2}} 1 \ \& \ f(x{'}) =_{\mathsmaller{\D 2}} 0 \big)
\]

If $f \in \D F(X, \D 2)$, the following extensional subsets of $X$

\[ \delta_0^1(f) := \{x \in X \mid f(x) =_{\mathsmaller{\D 2}} 1\}, \]

\[ \delta_0^0(f) := \{x \in X \mid f(x) =_{\mathsmaller{\D 2}} 0\}, \]

are called detachabledetachable subset, or freefree subset subsets of $X$. Let also
their pair $\B \delta (f) := \big(\delta_0^1(f), \delta_0^0(f)\big)$.

$  x \neq_X^{\mathsmaller{\D F(X, \D 2)}} x{'} \TOT \exists_{f \in \D F(X, \D 2)}\big(f(x) \neq_{\D 2} f(x{'})\big)$,
and $\B \delta (f)$ is a complemented subset of $X$ with respect to the inequality $\neq_X^{\mathsmaller{\D F(X, \D 2)}}$.
The characteristic function $\chi_{\B \delta(f)}$ of $\B \delta(f)$ is definitionally equal to $f$ (recall that
$f(x) =_{\mathsmaller{\D 2}} 1 :\TOT f(x) := 1$), and $\delta_0^1(f) \cup \delta_0^0(f) = X$.

If $\B A, \B B \in \C P^{\Disj}(X)$ and $\B C \in \C P^{\Disj}(Y)$,
let$\B A \cup \B B$$\B A \cap \B B$$- \B A$
$\B A - \B B$$\B A \times \B C$

\[ \B A \cup \B B  := (A^1 \cup B^1, A^0 \cap B^0), \]

\[ \B A \cap \B B := (A^1 \cap B^1, A^0 \cup B^0), \]

\[- \B A := (A^0, A^1), \]

\[ \B A - \B B := (A^1 \cap B^0, A^0 \cup B^1), \]

\[ \B A \times \B C := \big(A^1 \times C^1, \ [A^0 \times Y] \cup [X \times C^0]\big). \]

The following diagrams depict $\B A \cup \B B, \B A \cap \B B$, $\B A - \B B$, and $\B A \times \B C$, respectively.

(AO) at (1,3) ;
(BO) at (6,5) ;
(AZ) at (10,3) ;
(BZ) at (5,0) ;

plot [smooth cycle,tension=0.75] coordinates (AO) (3,4) (4,3) (4,1) (2,1)
plot [smooth cycle,tension=0.75] coordinates (0,4) (2,5) (BO) (9,4) (5,3)
plot [smooth cycle,tension=0.75] coordinates (6,3) (8,4) (AZ) (9,1) (7,1)
plot [smooth cycle,tension=0.75] coordinates (0,1) (2,2) (8,2) (8,0) (BZ) (2,0)

[scale=1,anchor=east] at (AO) $A^1$;
[scale=1,anchor=south] at (BO) $B^1$;
[scale=1,anchor=west] at (AZ) $A^0$;
[scale=1,anchor=north] at (BZ) $B^0$;

(AO) at (1,3) ;
(BO) at (6,5) ;
(AZ) at (8,3) ;
(BZ) at (5,0) ;

plot [smooth cycle,tension=0.75] coordinates (AO) (2,4) (3.5,3.5) (3,1) (1,1)
plot [smooth cycle,tension=0.75] coordinates (0.5,4) (2,5) (BO) (8,4) (5,3)
plot [smooth cycle,tension=0.75] coordinates (5,3) (6,4) (AZ) (7,1) (5,1)
plot [smooth cycle,tension=0.75] coordinates (0,1) (2,2) (7,2) (8,0) (BZ) (2,0)

[scale=1,anchor=east] at (AO) $A^1$;
[scale=1,anchor=south] at (BO) $B^1$;
[scale=1,anchor=west] at (AZ) $A^0$;
[scale=1,anchor=north] at (BZ) $B^0$;

(AO) at (0.5,3) ;
(BO) at (6,5) ;
(AZ) at (8,3) ;
(BZ) at (5,0) ;

plot [smooth cycle,tension=0.75] coordinates (AO) (2,4) (3.5,3.5) (3,1) (1,1)
plot [smooth cycle,tension=0.75] coordinates (0.5,4) (2,5) (BO) (8,4) (5,3) (2.5,3.5)
plot [smooth cycle,tension=0.75] coordinates (5,3) (6,4) (AZ) (7,1.5) (6,1)
plot [smooth cycle,tension=0.75] coordinates (0,1) (2,2) (6,2) (7,0) (BZ) (2,0)

[scale=1,anchor=east] at (AO) $A^1$;
[scale=1,anchor=south] at (BO) $B^1$;
[scale=1,anchor=west] at (AZ) $A^0$;
[scale=1,anchor=north] at (BZ) $B^0$;

(O) at (0,0) ;
(AOI) at (0.75,0) ;
(AOII) at (2.25,0) ;
(BOI) at (0,0.5) ;
(BOII) at (0,1.5) ;
(AZI) at (2.75,0) ;
(AZII) at (3.5,0) ;
(BZI) at (0,2) ;
(BZII) at (0,2.5) ;

(y) at (0,3);
(x) at (4,0);

(y) node[above left] $Y$ – (0,0) –  (x) node[below right] $X$;

[color=blue,opacity=0.3] (AOI |- BOI) rectangle (AOII |- BOII);
[color=red,opacity=0.3] (AZI |- O) rectangle (AZII |- BZI);
[color=red,opacity=0.3] (O |- BZI) rectangle (AZII |- BZII);
[color=red,opacity=0.3] (AZI |- BZII) rectangle (AZII |- y);
[color=red,opacity=0.3] (AZII |- BZI) rectangle (x |- BZII);

[color=black,thick] (AOI)++(0,-0.05) – (AOI |- 0,0.05);
[color=black,thick] (AOII)++(0,-0.05) – (AOII |- 0,0.05);
[color=black,thick] (BOI)++(-0.05,0) – (0.05,0 |- BOI);
[color=black,thick] (BOII)++(-0.05,0) – (0.05,0 |- BOII);

[color=black,thick] (AZI)++(0,-0.05) – (AZI |- 0,0.05);
[color=black,thick] (AZII)++(0,-0.05) – (AZII |- 0,0.05);
[color=black,thick] (BZI)++(-0.05,0) – (0.05,0 |- BZI);
[color=black,thick] (BZII)++(-0.05,0) – (0.05,0 |- BZII);

[color=black,dashed] (AOI) – (AOI |- BOII);
[color=black,dashed] (AOII) – (AOII |- BOII);
[color=black,dashed] (BOI) – (AOII |- BOI);
[color=black,dashed] (BOII) – (AOII |- BOII);

[color=black,dashed] (AZI) – (AZI |- y);
[color=black,dashed] (AZII) – (AZII |- y);
[color=black,dashed] (BZI) – (x |- BZI);
[color=black,dashed] (BZII) – (x |- BZII);

(AOII)++(0,-0.1) – (AOI |- 0,-0.1) node [black,midway,yshift=-0.7cm] $A^1$;
(AZII)++(0,-0.1) – (AZI |- 0,-0.1) node [black,midway,yshift=-0.7cm] $A^0$;

(BOI)++(-0.1,0) – (-0.1,0 |- BOII) node [black,midway,xshift=-0.7cm] $C^1$;
(BZI)++(-0.1,0) – (-0.1,0 |- BZII) node [black,midway,xshift=-0.7cm] $C^0$;

If $\B A, \B B \in \C P^{\mathsmaller{\Disj}}(X)$ and $\B C \in \C P^{\mathsmaller{\Disj}}(Y)$, then
$\B A \cup \B B$, $\B A \cap \B B$, $- \B A$, and $\B A - \B B$ are in $\C P^{\mathsmaller{\Disj}}(X)$
and $\B A \times \B C$ is in $\C P^{\mathsmaller{\Disj}} (X \times Y)$.

We show only the last membership. If $(a_1, b_1) \in A^1 \times B^1$ and $(a_0, b_0) \in A^0 \times B^0$,
then $i_{A^1}^X(a_1) \neq_X i_{A^0}^X(a_0)$ and $i_{B^1}^Y(b_1) \neq_Y i_{B^0}^Y(b_0)$. By definition

\[ i_{A^1 \times B^1}^{X \times Y}(a_1, b_1) := \big(i_{A^1}^X(a_1), i_{B^1}^Y(b_1)\big). \]

If $(a_0, y) \in A^0 \times Y$, then $(i_{A^0}^X \times \id_Y)(a_0, y) := (i_{A^0}^X(a_0), y)$, and if
$(x, b_0) \in X \times B^0$, then $(\id_X \times i_{B^0}^Y)(x, b_0) := (x, i_{B^0}^Y(b_0))$. In both
cases we get the required inequality.

Let $\B A, \B B$ and $\B C$ be in $\C P^{\mathsmaller{\Disj}} (X)$. The following hold:

$- (- \B A) := \B A$.

$- (\B A \cup \B B) := (- \B A) \cap (- \B B)$.

$- (\B A \cap \B B) := (- \B A) \cup (- \B B)$.

$\B A \cup (\B B \cap \B C) =_{\C P^{\mathsmaller{\Disj}} (X)} (\B A \cup \B B) \cap (\B A \cup \B C)$.

$\B A \cap (\B B \cup \B C) =_{\C P^{\mathsmaller{\Disj}} (X)} (\B A \cap \B B) \cup (\B A \cap \B C)$.

$\B A - \B B := \B A \cap (- \B B)$.

$\B A \subseteq \B B \TOT (\B A \cap \B B) =_{\C P^{\mathsmaller{\Disj}}(X)} \B A$.

$\B A \subseteq \B B \TOT - \B B \subseteq - \B A$.

If $\B A \subseteq \B B$ and $\B B \subseteq \B C$, then $\B A \subseteq \B C$.

Let $\B A \in \C P^{\mathsmaller{\Disj}}(X)$ and $B, C \in \C P^{\mathsmaller{\Disj}}(Y)$.

$\B A \times (\B B \cup \B C) =_{\C P^{\mathsmaller{\Disj}}(X \times Y)} (\B A \times \B B) \cup
(\B A \times \B C)$.

$\B A \times (\B B \cap \B C) =_{\C P^{\mathsmaller{\Disj}}(X \times Y)} (\B A \times \B B) \cap
(\B A \times \B C)$.

We prove only (i). We have that

\begin{align*}
\B A \times (\B B \cup \B C) & := (A^1, A^0) \times (B^1 \cup C^1, B^0 \cap C^0)\\
& := \big(A^1 \times (B^1 \cup C^1), (A^0 \times Y) \cup [X \times (B^0 \cap C^0)]\big)\\
& =_{\C P^{\mathsmaller{\Disj}}(X \times Y)}  \big((A^1 \times B^1) \cup (A^1 \times C^1), [(A^0 \times Y)
\cup (X \times B^0)] \ \cap\\
& \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \cap  [(A^0 \times Y) \cup (X \times C^0)]\big)\\
& := (\B A \times \B B) \times (\B A \times \B C).\qedhere
\end{align*}

Let the sets $(X, =_X, \neq_X^f)$ and $(Y, =_Y, \neq_Y)$, where $f \colon X \to Y$ $($see
Remark <ref>$)$.
Let also $\B A := (A^1, A^0)$ and $\B B := (B^1, B^0)$ in $\C P^{\mathsmaller{\Disj}} (Y)$.

$f^{-1}(\B A) := \big(f^{-1}(A^1), f^{-1}(A^0)\big) \in \C P^{\Disj} (X)$.

$f^{-1}(\B A \cup \B B) =_{\mathsmaller{\C P^{\Disj} (X)}}
f^{-1}(\B A) \cup f^{-1}(\B B)$.

$f^{-1}(\B A \cap \B B) =_{\mathsmaller{\C P^{\Disj} (X)}} f^{-1}(\B A) \cap f^{-1}(\B B)$.

$f^{-1}(- \B A) =_{\mathsmaller{\C P^{\Disj} (X)}} - f^{-1}(\B A)$.

$f^{-1}(\B A - \B B) =_{\mathsmaller{\C P^{\Disj} (X)}} f^{-1}(\B A) - f^{-1}(\B B)$.

(i) By Definition <ref> we have that

\[ f^{-1}(A^1) := \{(x, a_1) \in X \times A^1 \mid f(x) =_Y i_{A^1}^X (a_1)\}, \ \ \ \
i_{\mathsmaller{f^{-1}(A^1)}}^X(x, a_1) := x, \]

\[ f^{-1}(A^0) := \big(\{(x, a_0) \in X \times A^0 \mid f(x) =_Y i_{A^0}^X (a_0)\}, \ \ \ \
i_{\mathsmaller{f^{-1}(A^0)}}^X(x, a_0) := x. \]

Let $(x, a_1) \in f^{-1}(A^1)$ and $(z, a_0) \in f^{-1}(A^0)$. By the extensionality of $\neq_Y$ we have that

\[ i_{\mathsmaller{f^{-1}(A^1)}}^X(x, a_1) \neq_X^f i_{\mathsmaller{f^{-1}(A^0)}}^X(z, a_0)
:\TOT x \neq_X^f z :\TOT f(x) \neq_Y f(z) \TOT i_{A^1}^X (a_1) \neq_Y i_{A^0}^X (a_0), \]

and the last inequality holds by the hypothesis $\B A \in \C P^{\mathsmaller{\Disj}} (Y)$.
Next we show only (ii):

\begin{align*}
f^{-1}(\B A \cup \B B) & := f^{-1}\big(A^1 \cup B^1, A^0 \cap B^0 \big)\\
& := \big(f^{-1}(A^1 \cup B^1), f^{-1}(A^0 \cap B^0)\big)\\
& = \big(f^{-1}(A^1) \cup f^{-1}(B^1), f^{-1}(A^0) \cap f^{-1}(B^0)\big)\\
& := f^{-1}(\B A) \cup f^{-1}(\B B).\qedhere
\end{align*}

Alternatively, one can define the following operations between complemented subsets.

If $\B A, \B B \in \C P^{\Disj}(X)$ and $\B C \in \C P^{\Disj}(Y)$, let$\B A \vee \B B$$\B A \wedge \B B$
$\B A \ominus \B B$$\B A \otimes \B C$

\[ \B A \vee \B B := \big([A^1 \cap B^1] \cup [A^1 \cap B^0] \cup [A^0 \cap B^1], \ A^0 \cap B^0\big), \]

\[ \B A \wedge \B B := \big(A^1 \cap B^1, \ [A^1 \cap B^0] \cup [A^0 \cap B^1] \cup [A^0 \cap B^0]\big), \]

\[ \B A \ominus \B B := \B A \wedge (- \B B), \]

\[ \B A \otimes \B C := \big(A^1 \times C^1, \ [A^1 \times C^0] \cup [A^0 \times C^1] \cup [A^0 \times C^0]\big), \]

The following diagrams depict $\B A \vee \B B, \B A \wedge \B B$, $\B A \ominus \B B$, and $\B A \otimes \B C$,

(AO) at (1,3) ;
(BO) at (6,5) ;
(AZ) at (10,3) ;
(BZ) at (5,0) ;

plot [smooth cycle,tension=0.75] coordinates (AO) (3,4) (4,3) (4,1) (2,1)
plot [smooth cycle,tension=0.75] coordinates (0,4) (2,5) (BO) (9,4) (5,3)
plot [smooth cycle,tension=0.75] coordinates (6,3) (8,4) (AZ) (9,1) (7,1)
plot [smooth cycle,tension=0.75] coordinates (0,1) (2,2) (8,2) (8,0) (BZ) (2,0)

[scale=1,anchor=east] at (AO) $A^1$;
[scale=1,anchor=south] at (BO) $B^1$;
[scale=1,anchor=west] at (AZ) $A^0$;
[scale=1,anchor=north] at (BZ) $B^0$;

(AO) at (1,3) ;
(BO) at (6,5) ;
(AZ) at (10,3) ;
(BZ) at (5,0) ;

plot [smooth cycle,tension=0.75] coordinates (AO) (3,4) (4,3) (4,1) (2,1)
plot [smooth cycle,tension=0.75] coordinates (0,4) (2,5) (BO) (9,4) (5,3)
plot [smooth cycle,tension=0.75] coordinates (6,3) (8,4) (AZ) (9,1) (7,1)
plot [smooth cycle,tension=0.75] coordinates (0,1) (2,2) (8,2) (8,0) (BZ) (2,0)

[scale=1,anchor=east] at (AO) $A^1$;
[scale=1,anchor=south] at (BO) $B^1$;
[scale=1,anchor=west] at (AZ) $A^0$;
[scale=1,anchor=north] at (BZ) $B^0$;

(AO) at (1,3) ;
(BO) at (6,5) ;
(AZ) at (10,3) ;
(BZ) at (5,0) ;

plot [smooth cycle,tension=0.75] coordinates (AO) (3,4) (4,3) (4,1) (2,1)
plot [smooth cycle,tension=0.75] coordinates (0,4) (2,5) (BO) (9,4) (5,3)
plot [smooth cycle,tension=0.75] coordinates (6,3) (8,4) (AZ) (9,1) (7,1)
plot [smooth cycle,tension=0.75] coordinates (0,1) (2,2) (8,2) (8,0) (BZ) (2,0)

[scale=1,anchor=east] at (AO) $A^1$;
[scale=1,anchor=south] at (BO) $B^1$;
[scale=1,anchor=west] at (AZ) $A^0$;
[scale=1,anchor=north] at (BZ) $B^0$;

(O) at (0,0) ;
(AOI) at (0.75,0) ;
(AOII) at (2.25,0) ;
(BOI) at (0,0.5) ;
(BOII) at (0,1.5) ;
(AZI) at (2.75,0) ;
(AZII) at (3.5,0) ;
(BZI) at (0,2) ;
(BZII) at (0,2.5) ;
(y) at (0,3);
(x) at (4,0);

(y) node[above left] $Y$ – (0,0) –  (x) node[below right] $X$;

[color=blue,opacity=0.3] (AOI |- BOI) rectangle (AOII |- BOII);

[color=red,opacity=0.3] (AZI |- BOI) rectangle (AZII |- BOII);
[color=red,opacity=0.3] (AOI |- BZI) rectangle (AOII |- BZII);
[color=red,opacity=0.3] (AZI |- BZII) rectangle (AZII |- BZI);

[color=black,thick] (AOI)++(0,-0.05) – (AOI |- 0,0.05);
[color=black,thick] (AOII)++(0,-0.05) – (AOII |- 0,0.05);
[color=black,thick] (BOI)++(-0.05,0) – (0.05,0 |- BOI);
[color=black,thick] (BOII)++(-0.05,0) – (0.05,0 |- BOII);

[color=black,thick] (AZI)++(0,-0.05) – (AZI |- 0,0.05);
[color=black,thick] (AZII)++(0,-0.05) – (AZII |- 0,0.05);
[color=black,thick] (BZI)++(-0.05,0) – (0.05,0 |- BZI);
[color=black,thick] (BZII)++(-0.05,0) – (0.05,0 |- BZII);

[color=black,dashed] (AOI) – (AOI |- BOII);
[color=black,dashed] (AOII) – (AOII |- BOII);
[color=black,dashed] (BOI) – (AOII |- BOI);
[color=black,dashed] (BOII) – (AOII |- BOII);

[color=black,dashed] (AZI) – (AZI |- BZII);
[color=black,dashed] (AZII) – (AZII |- BZII);
[color=black,dashed] (BZI) – (AZII |- BZI);
[color=black,dashed] (BZII) – (AZII |- BZII);

(AOII)++(0,-0.1) – (AOI |- 0,-0.1) node [black,midway,yshift=-0.7cm] $A^1$;
(AZII)++(0,-0.1) – (AZI |- 0,-0.1) node [black,midway,yshift=-0.7cm] $A^0$;

(BOI)++(-0.1,0) – (-0.1,0 |- BOII) node [black,midway,xshift=-0.7cm] $C^1$;
(BZI)++(-0.1,0) – (-0.1,0 |- BZII) node [black,midway,xshift=-0.7cm] $C^0$;

With the previous definitions the corresponding characteristic functions are expressed through the characteristic
functions of
$\B A$ and $\B B$.

If $\B A, \B B$ are complemented subsets of $X$, then $\B A \vee \B B, \B A \wedge \B B, \B A - \B B$
and $- \B A$ are complemented subsets of $X$ with characteristic functions

\[ \chi_{\B A \vee \B B} =_{\C F(X, \D 2)} \chi_{\B A} \vee \chi_{\B B}, \  \ \chi_{\B A \wedge \B B} =_{\C F(X,
\D 2)} \chi_{\B A} \cdot \chi_{\B B}, \ \
\chi_{\B A - \B B} =_{\C F(X, \D 2)} \chi_{\B A}(1 - \chi_{\B B}), \ \ \ \]

\[ \chi_{\B A \otimes \B B}(x, y) =_{\C F(X \times X, \D 2)} \chi_{\B A}(x) \cdot \chi_{\B B}(y), \ \ \
\chi_{- \B A} =_{\C F(X, \D 2)} 1 - \chi_{\B A}.
\]

We show only the equality $\chi_{\B A \wedge \B B} =_{\C F(X, \D 2)} \chi_{\B A}
\cdot \chi_{\B B}$. By Definition <ref> the multiplication of the partial maps $\chi_{\B A} \colon
\Dm(\B A) \to \D 2$ and $\chi_{\B B} \colon \Dm(\B B) \to \D 2$ is
the partial function

\[ \chi_{\B A} \cdot \chi_{\B B} := \big(\Dm(\B A) \cap \Dm(\B B), i_{\Dm(\B A) \cap \Dm(\B B)}^X, (\chi_{\B A}
\cdot \chi_{\B B})_{\Dm(\B A) \cap \Dm(\B B)}^{\D 2} \big), \]

\[ (\chi_{\B A} \cdot \chi_{\B B})_{\Dm(\B A) \cap \Dm(\B B)}^{\D 2}(u, w) := \chi_{\B A}(u) \cdot \chi_{\B B}(w), \]

for every $(u, w) \in \Dm(\B A) \cap \Dm(\B B)$. The partial function $\chi_{\B A \wedge \B B}$ is the triplet

\[ \chi_{\B A \wedge \B B} := \big(\Dm(\B A \wedge \B B), i_{\Dm(\B A \wedge \B B)}^X, (\chi_{\B A
\wedge \B B})_{\Dm(\B A \wedge \B B)}^{\D 2} \big). \]

Since $\Dm(\B A \wedge \B B) =_{\C P(X)} \Dm(\B A) \cap \Dm(\B B)$, and if $(f, g) \colon \Dm(\B A \wedge \B B)
=_{\C P(X)} \Dm(\B A) \cap \Dm(\B B)$, it is straightforward to show that also the following outer diagram commutes

(E) at (0,0) $\Dm(\B A \wedge \B B)$;
[right=of E] (L) ;
[right=of L] (M) ;
[right=of M] (B) ;
[right=of B] (F) $\Dm(\B A) \cap \Dm(\B B)$;
[below=of M] (N) ;
[below=of N] (A) $X$;
[below=of A] (C) $\D 2$;

[->,bend left] (E) to node [midway,below] $f$ (F);
[->,bend left] (F) to node [midway,above] $g$ (E);
[->,bend right=50] (E) to node [midway,left] $(\chi_{\B A \wedge \B B})_{\Dm(\B A \wedge \B B)}^{\D 2} \ \ $ (C);
[->,bend left=50] (F) to node [midway,right] $ \ \ (\chi_{\B A} \cdot \chi_{\B B})_{\Dm(\B A) \cap \Dm(\B B)}^{\D 2}$ (C);
[right hook->,bend right=40] (E) to node [midway,right] $ \ i_{\Dm(\B A \wedge \B B)}^X$ (A);
[left hook->,bend left=40] (F) to node [midway,left] $i_{\Dm(\B A) \cap \Dm(\B B)}^X \ $ (A);

and hence the two partial functions are equal in $\C F(X, \D 2)$.

§ NOTES

In [55] Greenleaf introduced predicates on objects through the totality $\Omega$ of propositions
and then he defined $\C P(X)$ as $\D F(X, \Omega)$. A similar treatment of the powerset $\C P(X)$ is found
in [115]. For us a predicate on a set $X$ is a bounded formula $P(x)$ with $x$ as a free variable.
In order to define new objects from $X$ through $P$ we ask $P$ to be extensional.

In [27], pp. 114-5, Cantor described a set as follows:

A manifold (a sum, a set) of elements belonging to some conceptual
sphere is called well-defined if, on the basis of its definition and in
accordance with the logical principle of the excluded third, it must
be regarded as internally determined, both whether any object of
that conceptual sphere belongs as an element to the mentioned set,
and also whether two objects belonging to the set, in spite of formal
differences in the mode of givenness, are equal to each other or not.

Bishop's intuitive notion of set is similar to Cantor's, except that he does not invoke
the principle of the excluded middle ($\PEM$). As it was pointed to me by W. Sieg, Dedekind's
primitive notions in [44]  were “systems” and “transformations of systems”.

Notice that here we study defined totalities that are not defined inductively.
The inductively defined sets are expected to be studied in a future work within an extension $\BST^*$ of $\BST$.

Although $\Nat$ is the only primitive set considered in $\BST$, one

could, in principle, add more primitive sets. E.g., a primitive set of Booleans, of integers, and,
more interestingly, a primitive continuous interval, or a primitive real line (see [23] for an axiomatic
treatment of the set $\Real$ of reals within $\BISH$).

In Martin-Löf type theory the definitional, or judgemental equality $a := b$, where $a, b$ are terms
of some type $A$, is never used in a formula. We permit the use of the
definitional equality $:=$ for membership conditions only.
In the membership condition for the product we use the primitive notion of a pair.
The membership condition for an extensional subset $X_P$ of $X$ implies that an object $x$ “has not unique typing”,
as it can be an element of more than one sets.

The positively defined notion of discrete set used here comes from [76], p. 9. There it is also mentioned that
a set without a specified inequality i.e., a pair $(X, =_X)$, is discrete, if
$\forall_{x,y \in X}\big(x =_X y \ \vee \ \neg(x =_X y)\big)$.

In [84] it is mentioned that the above discreteness of $\D F(\Nat, \Nat)$ implies
the non-constructive principle “weak $\LPO$”

\[ \forall_{f \in \D F(\Nat, \Nat)}\bigg(\forall_{n \in \Nat}\big(f(n) =_{\Nat} 0\big) \ \vee \ \neg
\forall_{n \in \Nat}\big(f(n) =_{\Nat} 0\big)\bigg). \]

Because of a result of Bauer and Swan in [4], we cannot show in $\BISH$ the existence of an
uncountable separable metric space, hence, using the discrete metric, the existence of an uncountable
discrete set. Note that in [9], p. 66, a set $S$ is called discrete, if the set
$D := \{(s, t) \in S \times S \mid s=_S t\}$ is a freefree subset, or a detachabledetachable subset subset of $S \times S$.
In Definition <ref> we use the symbol $D(S)$ for $D$ and we call it the diagonal of $S$. We employ here the diagonal of a set in the fundamental definition of a set-indexed family of sets (Definition <ref>).

In [9] and [19], the negation $\neg \phi$ of a formula $\phi$ is not mentioned explicitly. E.g., the exact
writing of condition $(\Ap_1)$ in Definition <ref> is “if $x =_X y$ and $x \neq_X y$, then $0 =_{\Nat} 1$”.
Similarly, the condition of tightness in Definition <ref> is written as follows:
“if $x \neq_X y$ entails $0 = 1$, then $x =_X y$”. hence, if $\neq_X$ is tight, the implication $x \neq_X y \To
0 =_{\Nat} 1$ is logically equivalent to the (positively defined, if $X$ is a defined totality) equality $x =_X y$.
Within intuitionistic logic one defines $\neg \phi := \phi \To \bot$.

The definitions of $(-2)$-sets and $(-1)$-sets are proof-irrelevant translations of the corresponding notions in $\HoTT$,
which were introduced by Voevodsky (see [127]). The definition of a $0$-set requires to determine a set
$\Eq^X(x, y)$ of witnesses of the equality $x =_X y$. This is done in a universal way in $\MLTT$, while in $\BST$
in a “local” way, and by definition (see Definition <ref>).

In the literature of constructive mathematics (see e.g., [7], pp. 34–35)
the term preset is used for a totality.
Also, the term operation is used for a non-dependent assignment routine from a totality $X$ to a totality $Y$
(see [7], p. 44), while we use it only for a non-dependent assignment routine from a set $X$ to a set $Y$.

The notion of uniqueness associated to the definition of a function is local, in the following sense:
if $f \colon X \to Y$, it is immediate to show that $\forall_{x \in X}\exists!_{y \in Y}\big(f(x) =_Y y\big)$.

The converse is the local version of Myhill's axiom of non-choice $(\LANC)$. Let $P(x, y)$ be an extensional property on
$X \times Y$ i.e., $\forall_{x, x{'}, y, y{'} \in X}\big([x =_X x{'} \ \& \ y =_Y y{'} \ \& \ P(x, y)]
\To P(x{'}, y{'})\big)$. The principle
$(\LANC)$local version of Myhill's axiom of non-choice$(\LANC)$ is the formula

\[ \forall_{x \in X}\exists!_{y \in Y}P(x, y) \To \exists_{f \in \D F(X, Y)}\forall_{x \in X}\big(P(x,
f(x))\big). \]

Notice that $\LANC$ provides the existence of a function for which we only know how its outputs behave with
respect to the equality of $Y$, and it gives no information on how $f$ behaves definitionally.
If we define $Q_x  (y) : = P(x, y)$, then if we suppose $Q_x (f(x))$ and $Q_x (g(x))$, for some $f, g \in
\D F(X, Y)$, we get $f(x) =_Y y =_Y g(x)$, and then $(\LANC)$ implies

\[ \forall_{x \in X}\exists!_{y \in Y}P(x, y) \To \exists!_{f \in \D F(X, Y)}\forall_{x \in X}\big(P(x,
f(x))\big). \]

We can use $(\LANC)$ to view an arbitrary subset $(A, i_A^X)$ of $X$ as an extensional subset of $X$.
If $(A, i_A^X) \in \C P(X)$, then the property $P_A$ on $X$ defined by
$P_A(x) :=  \exists_{a \in A}\big(i_A^X (a) =_X x\big)$,

is extensional, and $(i_A^X, j_A^{X}) : X_{P_A} =_{\C P(X)} (A, i_A^X)$, for some function $j_A^{X} \colon X_{P_A} \to A$.
To show this, let $x, y \in X$ such that $P_A(x)$ and $x =_X y$. By transitivity of $=_X$, if $i_A^{X} (a) =_X x$, then
$i_A^{X} (a) =_X y$. If $x \in X$ and $a, b \in A$ such that $i_A^{X} (a) =_X x =_X i_A^{X} (b)$, then $a =_A b$ i.e.,
$\forall_{x \in X_{P_A}}\exists!_{a  \in A}\big(i_A^{X} (a) =_X x\big)$,

and since the property $Q(x, a) : \TOT i_A^{X} (a) =_X x$ is extensional on $X_{P_A} \times A$, by $(\LANC)$
there is  a (unique) function $j_A^{X} : X_{P_A} \to A$, such that for every $x \in X_P$ we have that
$i_A^X(j_A ^{X}(x)) =_X x$, and the required diagram commutes.
The principle $(\LANC)$, which is also considered in [5], is included in Myhill's system $\CST$ (see [80])
as a principle of generating functions. This is in contrast to Bishop's algorithmic approach to the concept of

In [19], p. 67, a function $f : A \to B$ is defined as a finite routine which,
applied to any element of $A$, produces an element $b \equiv f(a)$ of $B$, such that $f(a) =_B f(a{'})$,
whenever $a =_A a{'}$. In [19], p. 15, we read that $f$ “affords an explicit, finite mechanical reduction
of the procedure for
constructing $f(a)$ to the procedure for constructing $a$”.
The pattern of defining a function $\fXY$ by first defining an operation $f \colon X \sto Y$, and then proving that
$f$ is a function, is implicit in the more elementary parts of [9] and [19], and more explicit
in the later parts of the books. E.g., in [19], p. 199, an inhabited subset $U$ of
$\D C$ has the maximal extent property, if there
is an operation $\mu$ from $U$ to $\Real^+$ satisfying certain properties. One can show afterwords
that $U$ is open and $\mu$ is a function on $U$. This property is used in Bishop's proof
of the Riemann mapping theorem (see [19], pp. 209–210).

Regarding the set-character of $\D F(X, Y)$, Bishop, in [19], p. 67, writes:

When $X$ is not countable, the set $\D F(X, Y)$ seems to have little practical interest, because
to get a hold on its structure is too hard. For instance, it has been asserted by Brouwer that all
functions in $\D F(\Real, \Real)$ are continuous, but no acceptable proof of this assertion is known.

Similar problems occur though, in function spaces where the domain of the functions is
a countable set. E.g., we cannot accept constructively (i.e., in the sense of Bishop) that the Cantor
space $\D F(\Nat, 2)$ satisfies Markov's principle, but no one that we know of has doubted the
set-character of $\D F(\Nat, 2)$. The possibility of doubting the set-character of the Baire space $\D F(\Nat, \Nat)$
is discussed by Beeson in [7], p. 46.

In intensional Martin-Löf Type Theory the type

\[\bigg(\prod_{x \colon X}f(x) = g(x)\bigg) \to f = g \]

is not provable (inhabited), and its inhabitance is known as the
axiom of function extensionalityaxiom of function extensionality $(\FunExt)$$(\FunExt)$.
In $\BST$ this axiom is part of the canonical definition of the function space $\D F(X, Y)$. Because of this,
many results in $\MLTT + \FunExt$ are translatable in $\BST$ (see Chapter <ref>

The totality $\D V_0$ is not mentioned by Bishop, although it is necessary, if we want to formulate the
fundamental notion of a set-indexed family of sets.

The defined
equality on the universe $\D V_0$ expresses that $\D V_0$ is univalent, as isomorphic sets are
equal in $\D V_0$. In univalent type theory, which is $\MLTT$ extended with Voevodsky's
axiom of univalenceaxiom of univalence $\UA$$\UA$
(see [127]), the existence of a pair of quasi-inverses between types $A$ and $B$ implies
that they are equivalent in Voevodsky's sense, and by the univalence axiom, also propositionally equal.
The axiom $\UA$ is partially translated in $\BST$ as the canonical definition of $\D V_0$.
Because of this, results in $\MLTT + \UA$ that do not raise the level of the universe are translatable in $\BST$.
For example, Proposition <ref> is lemma 4.9.2 in book HoTT [127], where $\UA$ is used
in its proof: if $e \colon X \simeq Y$, then $Z \to X \simeq Z \to Y$, and by
$\UA$ we get $e = \idtoeqv (p)$, for some $p \colon X =_{\C U} Y$. Notice that in the
formulation of this lemma the universe-level is not raised.

The notion of a dependent operation is explicitly mentioned by Bishop in [9], p. 65, and
repeated in [19], p. 70, in the definition of the intersection of a family of subsets of a set
indexed by some set

an element $u$ of $\bigcap_{t \in T}\lambda(t)$ is a finite routine which
associates an element $x_t$ of $\lambda(t)$ with each element $t$ of $T$, such that
$i_t(x_t) = i_{t{'}}(x_{t{'}})$ whenever $t, t{'} \in T$.

This definition corresponds to our Definition <ref>.

Bishop's definition of a subset of a set is related to the notion of a subobject in Category Theory
(see [3], p. 89, and [54], p. 75). In practice the subsets of a set $X$ are defined through an
extensional property on $X$. In [20], p. 7, this approach to the notion of a subset is considered
as its definition. Note
that there the implication $x =_{X} y \To (P(y) \To P(x))$ is also included in
the definition of an extensional property, something which follows though, from the symmetry of $=_X$.
Such a form of separation axiom is used implicitly in [9] and in [19]. Myhill used in
his system $\CST$ the axiom of bounded separation to implement the notion of an extensional subset of $X$.
This axiom is also
included in Aczel's system $\CZF$ (see [1], p. 26).

One could have defined the equality $=_{A \cup B}$ without relying on the non-dependent assignment routine
$i_{A \cup B}^X$. If we define first

$$z =_{A \cup B} w  : \TOT \left\{ \begin{array}{lllllll}
i_A^X (z)  =_X i_A (w)  &\mbox{, $z, w \in A$}\\
i_A^X (z)  =_X i_B (w)  &\mbox{, $z \in A \ \& \ w \in B$}\\
i_B^X (z)  =_X i_B (w)  &\mbox{, $z, w \in B$}\\
i_B^X (z)  =_X i_A (w)  &\mbox{, $z \in B \ \& \ w \in A$,}
\end{array}
\right.$$

we can define afterwords the operation $i_{A \cup B}^X : A \cup B \to X$ as in
Definition <ref>.
In this way the non-dependent assignment routine $i_{A \cup B}^X$ is defined on a set, and it is an operation.
Bishop avoids this definition, probably because this pattern cannot be extended to the definition of a union of a family of
subsets (see Definition <ref>). In that case,
we cannot write down the corresponding case distinction for $z =_{A \cup B} w$. Moreover,
the proof of $\big(A \cup B, i_{A \cup B}^X\big) \subseteq X$ is immediate, if one
uses Definition <ref>.

The definition of the empty subset $\emptyset_X$ of a set $X$, given in [9], p. 65, can be
formulated as follows. Let $X$ be a set and $x_0 \in X$. The totality $\emptyset_X$ is defined by
$z \in \emptyset_X : \TOT x_0 \in X \ \& \ 0 =_{\Nat} 1$.

Let $i_{\emptyset}^X \colon \emptyset_X \sto X$ be the non-dependent assignment routine, defined by $i(z) := x_0$,
for every $z \in \emptyset_X$, and let $z =_{\emptyset_X} w : \TOT i(z) =_X i(w) : \TOT x_0 =_X x_0.$

The pair $(\emptyset_X, i_{\emptyset}^X)$ is the empty subsetempty subset of a set of $X$.
One can show that $=_{\emptyset_X}$ is an equality on $\emptyset_X$, and hence $\emptyset_X$ can be
considered to be a set. The assignment routine $i_{\emptyset}^X$ is an embedding of $\emptyset_X$ into $X$, and hence
$(\emptyset_X, i_{\emptyset}^X)$ is a subset of $X$. As Bishop himself writes in [9], p. 65, “the definition
of $\emptyset$ is negativistic, and we prefer to mention the void set as seldom as possible”.
In [19], p. 69, Bishop and Bridges define two subsets $A, B$ of $X$ to be disjoint, when
$A \cap B$ “is the void subset of $X$”.

Clearly, this “is” cannot be $A \cap B := \emptyset_X$. If we interpret it as
$A \cap B =_{\C P(X)} \emptyset_X$, we need the existence of certain functions
from $\emptyset_X$ to $A \cap B$ and from $A \cap B$ to $\emptyset_X$. The latter approach is
followed in $\MLTT$ for the empty type. Following Bishop, we refrain from elaborating this negatively defined notion.

If $(A, i_A^X) \subseteq A$, $(B, i_B^Y) \subseteq Y$, and $\fXY$, the
extensional imageextensional image $f[A]$$f[A]$ of
$A$ under $f$ is defined through the extensional property
$P(y) := \exists_{a \in A}\big(f(i_A(a)) =_Y y\big)$.
Similarly, the extensional pre-imageextensional pre-image $f^{-1}[B]$$f^{-1}[B]$ of
$B$ under $f$ is defined through the extensional property
$Q(x) := \exists_{b \in B}\big(f(x) =_Y i_B (b)\big)$.
The subset $f(A)$ of $Y$ contains exactly the outputs $f(i_A^X(a))$ of $f$, for every $a \in A$, while
the subset $f[A]$ of $Y$ contains all the elements of $Y$ that are $=_Y$-equal to some output  $f(i_A(a))$
of $f$, for every $a \in A$. It is useful to keep the “distinction” between the subsets  $f(A)$, $f[A]$, and
$f^{-1}(B)$, $f^{-1}[B]$.

We need the equality in $\C P(X)$ of a subset of $X$ to its extensional version (see Note <ref>),
hence the principle $\LANC$, to get
$f(A) =_{\C P(Y)} f[A]$ and $f^{-1}(B) =_{\C P(X)} f^{-1}[B]$.

There are instances in Bishop's work indicating that the powerset of a set is treated as a set.
In [9], p. 68, and in [19], p. 74,
the following “function” is defined

\[j : \C P^{\Disj} (X) \to \C P(X), \ \ \ \ (A^1, A^0) \mapsto A^1. \]

This is in complete contrast to our interpretation of a function as an operation between sets. Of course,
such a rule is an exception in [9] and [19].
In the definition of an integration space, see [19], p. 216, the “set” $\C F(X,Y)$ of all
strongly extensional partial functions from $X$ to $Y$ requires quantification over $\D V_0$.
Such a quantification is also implicit in the definition of a measure space given in [19], p. 282,
and in the definition of a complete measure space
in [19], p. 289. These definitions appeared first in [18], p. 47, and p. 55, respectively.
The powerset is repeatedly used as a set in [20] and [76]. It is not known if the treatment
of the powerset as a set implies some constructively unacceptable principle.

There are instances in Bishop's work indicating that the powerset of a set is not treated as a set.
See e.g., the definition of a set-indexed family of sets in [19], p. 78 (our Definition <ref>).
Similarly, in the definition of a family of subsets of a set $A$ indexed
by some set $T$ (see [19], p. 69), the notion of a finite routine that assigns a
subset of $A$ to an element of $T$ is used, and not the notion of a function from $T$ to $\C P (A)$.
In the definition of a measure space in [9], p. 183, a subfamily of a given family of
complemented sets is considered in order to avoid quantification over the class of all complemented subsets in the
formulations of the definitional clauses of a measure space (see Note <ref>).
The powerset axiom is also avoided in Myhill's formalization [80] of $\BISH$ and in Aczel's subsequent system
$\CZF$ of constructive set theory (see [1]). Although, as we said, it is not known if the use
of the powerset as a set implies some constructively unacceptable principle, it is not accepted in
any predicative development of constructive mathematics.

The notion of a partial function was introduced by Bishop and Cheng in [18], p. 1, and this definition,
together with the introduced term “partial function”, was also included in Chapter 3
of [19], p. 71. The totality of partial functions $\C F(X)$ from a set $X$ to $\Real$ is crucial to the
definition of an integration space in the new measure theory developed in [18], and seriously
extended in [19]. Only the basic algebraic operations on $\C F(X)$ were defined
in [19], p. 71. The composition of partial functions is mentioned in [39],
pp. 66–67.
A notion of a partial dependent operation can be defined as follows. If $A, I$ are sets, a partial dependent
operationpartial dependent operation is a triplet $(A, i_A^I, \Phi_A^{\lambda_0})$, where
$(A, i_A) \subseteq I$, $\lambda_0 \colon A \sto \D V_0$, and $\Phi_A^{\lambda_0} \colon
\bigcurlywedge_{a \in A}\lambda_0(a)$. If $\lambda_0(a) := Y$, for every $a \in A$, then the corresponding
partial dependent operation is reduced to a partial function in $\C F(I, Y)$.

In the study of various subsets of a set $X$ we avoided to define the complement of a subset,
since this requires a negative definition. Recall that the negatively defined notion of empty subset of a set
is not really used.  In [9] Bishop introduced a
positive notion of the complement of a subset of a set $X$, the notion of a complemented subset of $X$. For
its definition we need a notion of a fixed inequality on $X$, which is compatible with the given equality of
$X$. In this way we can express the disjointness of two subsets $A, B$ of a set $X$ in a positive way. Usually,
$A, B$ are called disjointdisjoint subsets, if $A \cap B$ is not inhabited.
It is computationally more informative though, if a positive way is found to express disjointness of subsets.
In [25] a positive notion of apartness is used as a foundation of constructive topology.

The definitions of $\B A \cap \B B, \B A \cup \B B$ and $\B A - \B B$ appear in [9], p. 66,
where $\B A \cup \B B$ and $\B A \cap \B B$ are special cases of the complemented subsets
$\bigcup_{i \in I}\B \lambda_0(i)$ and $\bigcap_{i \in I}\B \lambda_0(i)$, respectively (see Proposition <ref>). There the inequality on $X$ is induced by an inhabited set of functions from $X$ to $\Real$. The
definition of $\B A \times \B C$ appears in [9], p. 206, in the section of the product measures.
One can motivate these definitions applying a “classical” thinking. If $x \in X$, recall the definitions

\[ x \in \B A :\TOT x \in A^1 \ \ \ \& \ \ \ x \notin \B A :\TOT x \in A^0. \]

Interpreting the connectives in a classical way, we get

\[ x \in \B A \cup \B B \TOT x \in \B A  \ \vee  \ x \in \B B :\TOT x \in A^1 \ \vee  \ x \in B^1
:\TOT x \in A^1 \cup B^1, \]

\[ x \notin \B A \cup \B B \TOT x \notin \B A \ \& \ x \notin \B B :\TOT x \in A^0 \ \& \ x \in B^1
:\TOT x \in A^1 \cap B^1, \]

\[ x \in \B A \cap \B B \TOT x \in \B A  \ \&  \ x \in \B B :\TOT x \in A^1 \ \&  \ x \in B^1
:\TOT x \in A^1 \cap B^1, \]

\[ x \notin \B A \cap \B B \TOT x \notin \B A \ \vee \ x \notin \B B :\TOT x \in A^0 \ \vee \ x \in B^1
:\TOT x \in A^1 \cup B^1, \]

\[ x \in - \B A \TOT x \notin \B A :\TOT x \in A^0 \ \ \ \ \& \ \ \ \ x \notin - \B A \TOT x \in \B A
:\TOT x \in A^1, \]

\[ (x,y) \in \B A \times \B C \TOT x \in \B A \ \& \ y \in \B C :\TOT x \in A^1 \ \& \ y \in B^1 :\TOT
(x,y) \in A^1 \times B^1,\]

\[ (x,y) \notin \B A \times \B C \TOT x \notin \B A \ \vee \ y \notin \B C :\TOT x \in A^0 \ \vee \ y
\in B^0 :\TOT (x,y) \in (A^0 \times Y) \cup (X \times B^0).\]

In [18], pp. 16–17, and in [19], p. 73,
the operations between the complemented subsets of a set $X$ follow Definition <ref>
in order to employ the good behaviour of the corresponding characteristic functions in the new measure theory.
In the measure theory of [9], where the characteristic functions of complemented subsets are not crucial,
the operations between complemented subsets are defined according to Definition <ref>.

Bishop and Cheng use the notation $\B A \times \B B$ instead of $\B A \otimes \B B$.

As it is evident from the previous figures, the $1$- and $0$-components of the complemented subsets in the Bishop-Cheng definition are subsets of the corresponding $1$- and $0$-components of the complemented subsets in the Bishop definition from [9].  Actually, the definitions of the operations of complemented subsets
in [9] associate to the $1$-component of the complemented subset a maximal complement. The two sets of operations though, share the same algebraic and set-theoretic properties. They only behave differently
with respect to their characteristic functions.
Based on the work [115] of Shulman, we can motivate the second set of operations in a way similar to
the motivation provided for the first set of operations in Note <ref>.
Keeping the definitions of $x \in \B A$ and $x \notin \B B$, we can apply a “linear”
interpretation of the connectives $\vee$ and $\&$. As it is mentioned in [115], p. 2, the multiplicative
version $P \ \parl \ Q$$P \ \parl \ Q$ of $P \vee Q$ in linear logic  represents the pattern
“if not $P$, then $Q$; and if not $Q$, then $P$”. Let

\[ x \in \B A \vee \B B  :\TOT [x \notin \B A \To x \in \B B] \ \& \ [x \notin \B B \To x \in \B A]. \]

With the use of Ex falsum quodlibet the implication $x \notin \B A \To x \in \B B$ holds if $x \in \B A :\TOT x \in A^1$, or
if $x \notin \B A :\TOT x \in A^0$ and $x \in \B B :\TOT x \in B^1$ i.e., if $x \in A^0 \cap B^1$. Hence,
the first implication holds if $x \in A^1 \cup (A^0 \cap B^1)$. Similarly, the second holds if
$x \in B^1 \cup (B^0 \cap A^1)$. Thus

\[ x \in \B A \vee \B B \TOT x \in [ A^1 \cup (A^0 \cap B^1)] \cap [B^1 \cup (B^0 \cap A^1)], \]

and the last intersection is equal to $\Dm(\B A \vee \B B)$! One then can define $x \notin \B A \vee \B B
:\TOT x \notin \B A \ \& \ x \notin \B B$, and $x \in \B A \wedge \B B :\TOT x \in \B A \ \& \ x \in \B B$,
and $x \notin \B A \wedge \B B :\TOT x \in (- \B A) \vee (- \B B)$.

For the relation of complemented subsets to the Chu construction see [103].

CHAPTER: FAMILIES OF SETS

We develop the basic theory of set-indexed families of sets and of family-maps between them.
We study the exterior union of a family of sets $\Lambda$, or the $\sum$-set of $\Lambda$, and the set
of dependent functions over $\Lambda$, or the $\prod$-set of $\Lambda$. We prove the distributivity of
$\prod$ over $\sum$ for families of sets indexed by a product of sets, which is the translation
of the type-theoretic axiom of choice into $\BST$. Sets of sets are special set-indexed families of sets
that allow “lifting” of functions on the index-set to functions on them. The direct families of sets and the
set-relevant families of sets are introduced. The index-set of the former is a directed set, while the
transport maps of the latter are more than one and appropriately indexed. With the use of the introduced
universe $\D V_0^{\im}$ of sets and impredicative sets we study families of families of sets.

§ SET-INDEXED FAMILIES OF SETS

Roughly speaking, a family of sets indexed by some set $I$ is an

assignment routine $\lambda_0 : I \sto \D V_0$ that
behaves like a function i.e., if $i =_I j$, then $\lambda_0(i) =_{\D V_0} \lambda_0 (j)$. Next follows
an exact formulation of this description that reveals the witnesses of the
equality $\lambda_0(i) =_{\D V_0} \lambda_0 (j)$.

If $I$ is a set,
a family of setsfamily of sets indexed by $I$, or an $I$-family
of sets$I$-family of sets, is a pair $\Lambda := (\lambda_0, \lambda_1)$, where$\lambda_0$
$\lambda_0 \colon I \sto \D V_0$, and$\lambda_1$ $\lambda_1$, a
modulus of function-likeness formodulus of function-likeness $\lambda_0$, is given by

\[ \lambda_1 \colon \bigcurlywedge_{(i, j) \in D(I)}\D F\big(\lambda_0(i), \lambda_0(j)\big),
\ \ \ \lambda_1(i, j) := \lambda_{ij}, \ \ \ (i, j) \in D(I), \]

such that the transport mapstransport map of a family of sets $\lambda_{ij}$
transport map of a family of sets$\lambda_{ij}$
of $\Lambda$ satisfy the following conditions:

For every $i \in I$, we have that $\lambda_{ii} := \id_{\lambda_0(i)}$.

If $i =_I j$ and $j =_I k$, the following diagram commutes

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

[above=of E] (D) $\lambda_0(i)$;

[->] (E)–(F) node [midway,below] $\lambda_{jk}$;

[->] (D)–(E) node [midway,left] $\lambda_{ij}$;
[->] (D)–(F) node [midway,right] $\ \lambda_{ik}$;

$I$ is the index-setindex-set of the family $\Lambda$.

If $X$ is a set, the constant $I$-family of setsconstant family of sets
$X$$C^X$ is the pair
$C^X := (\lambda_0^X, \lambda_1^X)$, where $\lambda_0 (i) := X$, for every
$i \in I$, and $\lambda_1 (i, j) := \id_X$, for every $(i, j) \in D(I)$ $($see the left diagram in
Definition <ref>$)$.

The dependent operation $\lambda_1$ should have been written as follows

\[ \lambda_1 \colon \bigcurlywedge_{z \in D(I)}\D F\big(\lambda_0(\prb_1(z)), \lambda_0(\prb_2(z))\big), \]

but, for simplicity, we avoid the use of the primitive projections $\prb_1, \prb_2$. Condition (a) of
Definition <ref> could have been written as $\lambda_{ii} =_{\mathsmaller{\D F(\lambda_0(i),
\lambda_0(i))}} \id_{\lambda_0(i)}$. If $i =_I j$, then by conditions (b) and (a) of Definition <ref>
we get
$id_{\lambda_0(i)} := \lambda_{ii} = \lambda_{ji} \circ \lambda_{ij}$ and
$ \id_{\lambda_0(j)} := \lambda_{jj} = \lambda_{ij} \circ \lambda_{ji} $

i.e., $(\lambda_{ij}, \lambda_{ji}) \colon \lambda_0 (i) =_{\D V_0} \lambda_0 (j)$. In this sense $\lambda_1$ is
a modulus of function-likeness for $\lambda_0$.