Complemented subsets and Boolean-valued,partial functions

Abstract

We study the two algebras of complemented subsets that were introduced in the constructive development of the Daniell approach to measure and integration within Bishop-style constructive mathematics. We present their main properties both for the so-called here categorical complemented subsets and for the extensional complemented subsets. We translate constructively the classical bijection between subsets and Boolean-valued, total functions by establishing a bijection between complemented subsets (categorical or extensional) and Boolean-valued, partial functions (categorical or extensional). The role of Myhill’s axiom of non-choice in the equivalence between categorical and extensional subsets is discussed. We introduce swap algebras of type (I) and (II) as an abstract version of Bishop’s algebras of complemented subsets of type (I) and (II), respectively, and swap rings as an abstract version of the structure of Boolean-valued partial functions on a set. Our examples of swap algebras and swap rings together with the included here results indicate that their theory is a certain generalisation of the theory of Boolean algebras and Boolean rings, a fact which we find interesting both from a constructive and a classical point of view.

Keywords

Constructive mathematics Bishop set theory complemented subsets partial functions swap algebras

1. Introduction

In his reconstruction of constructive mathematics $BISH$ in [3] Bishop defined for a set X, equipped with an equality $=_{X}$ and an inequality $\neq_{X}$ , a positive notion of disjoint subsets of X and through the latter the concept of a complemented subset of X. Complemented subsets are easier to handle than plain subsets, as their partial, characteristic functions are constructively defined and their complement behaves a lot like the classical complement of a subset. These two features of complemented subsets were crucial to Bishop’s reconstruction of measure theory (BMT) in [3] and in Bishop-Cheng measure theory (BCMT), a constructive counterpart to the classical Daniell approach to measure theory, developed first in [5] and extended significantly in [4]. The two different measure theories of Bishop involve different operations between complemented subsets. In BMT the, so-called here, first algebra of complemented subsets is considered, while in $BCMT$ the second. As we explain here, the exact properties of these two algebras depend on the underlying theory of Bishop sets and subsets.

“Official” Bishop Set Theory (BST),1

¹
The type-theoretic interpretation of Bishop’s set theory into the theory of setoids [29,30] is nowadays the standard way to understand Bishop sets. A categorical interpretation of Bishop sets is Palmgren’s constructive adaptation [28] of Lawvere’s elementary theory of the category of sets. In [13] Coquand views Bishop sets as a natural sub-presheaf of the universe in the cubical set model.

presented in a condensed way in Chapter 3 of [3,4], and reconstructed in [32,34,36,38], motivated Martin-Löf’s type theory (MLTT) [22–24] and most of the formal studies of the 70’s (see [2]). In [3] Bishop defined subsets of a set in a categorical manner, as subobjects of an object in a category, and he defined the intersection of subsets through a standard pullback construction. For this reason, we call here these subsets categorical. The notion of a categorical subset (see Definition 2.2) is a proof-relevant approach to the notion of subset, as in its definition, and also in the definition of the inclusion relation ⊆ between subsets, certain functions are given as witnesses of the inclusion relations. As a consequence,2

The presence of a functions witnessing the inclusion relation of a set A into a given set X forces us to work with concrete terms, rather than logically, as in the case of an extensional subset. In the latter case Ex Falso is used in many cases.

minimal logic (MIN), rather than intuitionisitic logic (INT) is used in the proofs of the related facts, and the categorical powerset

P (X)

is a proper class, as its membership condition requires quantification over the universe

V_{0}

of predicative sets. Notice that Bishop never defined the empty set, only the categorical empty subset of an inhabited set.3

As Bishop writes in [3], p. 65, “the definition of $\emptyset_{X}$ is negativistic, and we prefer to mention the void set as seldom as possible”.

Moreover, dependent assignment routines are necessary to the definition of the notion of a set-indexed family of categorical complemented subsets (see Definition 2.8).

However, in practice Bishop worked mainly with the so-called here extensional subsets of a set X i.e., subsets of X defined by the separation scheme on extensional, bounded formulas $P (x)$ on X (see Definition 4.1). Every extensional subset is a categorical one, but for the converse the questionable, from a strict constructive point of view, Myhill’s axiom of non-choice4

⁴

Also known as Myhill’s axiom of unique choice.

(MANC) is required (see Proposition 6.1(iii)). The sufficiency of extensional subsets in the practice of

BISH

(see also [45]) led constructivists, such as Bridges and Richman, to work only with these. In what we call here Bridges-Richman Set Theory (BRST) only extensional subsets are employed.5

⁵

See [8], p. 7, [25], p. 7, while in [9], p. 12, the separating property P need not be extensional.

The use of extensional subsets is a proof-irrelevant and rather logical approach to the notion of subset, as relations and operations on subsets are governed by logical manipulations (see Definition 4.6) within

INT

, rather than within

MIN

. The extensional powerset

E (X)

was treated by Bridges and Richman as an impredicative set, and as we explain in Section 4, this is a sensible choice, if

MANC

is not accepted. A completely positive notion of an extensional empty subset of an arbitrary set with inequality is possible within the extensional framework (see Definition 4.2). Moreover, the notion of a set-indexed family of extensional subsets of a set does not require dependent assignment routines6

⁶

Dependent assignment routines are not used in $BRST$ . Instead, some basic category theory is employed in [25], p. 18, which is not developed though, within $BISH$ . The necessity of dependent assignment routines in $BISH$ is highlighted in [32]. The empty set is freely used in $BRST$ .

(see Definition 4.6).

In order to explain how the categorical (logical) nature of the categorical (extensional) subsets affect the properties of the corresponding algebras of complemented subsets and Boolean-valued partial functions, we treat the basic theory of categorical and extensional subsets separately, and we highlight the role of Myhill’s axiom of non-choice to their relation. We show in both frameworks that the pair of notions (complemented subsets, Boolean-valued partial functions) is the constructive analogue to the classical pair (subsets, Boolean-valued total functions). The abstract formulation of the properties of Bishop’s algebras of complemented subsets leads us to the notions of swap algebras of type (I) and (II), while the abstract formulation of the Boolean-valued, partial functions leads us to the notion of swap ring. The general properties of swap algebas and swap rings stem more naturally from the algebras of complemented extensional subsets and extensional partial functions We include various examples and basic results on swap algebras and swap rings, which indicate that their theory is a certain generalisation of the theory of Boolean algebras and Boolean rings, a fact which we find interesting both from a constructive and a classical point of view.

We structure this paper as follows:

In Section 2 we describe the basic theory of categorical subsets $P (X)$ of a set X, of complemented categorical subsets $P^{) (} (X)$ of X, and of Boolean-valued, categorical partial functions $F (X, 2)$ on X. We translate constructively the classical bijection between subsets and Boolean-valued functions by defining a proper-class equivalence between the proper classes $P^{) (} (X)$ and $F (X, 2)$ (Proposition 2.14).

In Section 3 we describe the two algebras of complemented categorical subsets, and we present some of their basic properties.

In Section 4 we describe the basic theory of extensional subsets $E (X)$ of a set X with an inequality, of complemented extensional subsets $E^{] [} (X)$ of X, and of Boolean-valued, extensional partial functions $F (X, 2)$ on X. The presence of an extensional inequality on X gives us the possibility to define the associated notions of an extensional empty subset, of ‘being empty’, and of disjointness in a completely positive way, avoiding negation.

In Section 5 we describe the two algebras of complemented extensional subsets, and we present their basic properties. A proof of the fact that Bishop’s distributivity property $(D_{N})$ implies the limited principle of omniscience $(LPO)$ , which avoids the empty set, is included.

In Section 6 we highlight the role of Myhill’s axiom of non-choice (MANC) to the relation between $P (X)$ and $E (X)$ . We introduce the notion of Myhill categorical subset the class of which is between the extensional powerset and the categorical one.

In Section 7 we introduce the notions of a swap algebra of type (I) and (I) as the abstract version of the two algebras of complemented extensional subsets. Various examples of swap algebras from logic, measure theory, and arithmetic are presented, and their fundamental properties are shown. The total elements of a swap algebra form a Boolean algebra, and every Boolean algebra is a swap algebra of both types (Proposition 7.10).

In Section 8 we introduce the notion of a swap ring as the abstract version of Boolean-valued, extensional partial functions. The fundamental properties of swap rings are shown. The total elements of a swap ring form a Boolean ring, and every Boolean ring is a swap ring (Proposition 8.5). The standard duality between Boolean algebras and Boolean rings is extended to a duality between swap algebras of type (II) and swap rings (Proposition 8.6).

In Section 9 we list some topics of future work.

This paper is an extension and improvement7

⁷

Only Sections 2, 3, the notion of the extensional empty subset in Section 4, and Proposition 5.2 are related to [42]. The rest of this paper is new. Moreover, the separation between the categorical and extensional framework followed here avoids the mixture of extensional subsets with categorical ones, especially the mixture of the extensional empty subset with operations between categorical subsets, which is found in [42].

of [42]. For all notions and results from

BST

that are used here without explanation or proof, we refer to [32,34,36]. For all notions and results from constructive analysis that are used here without explanation or proof we refer to [3,4]. In a proposition we write (INT) to denote that its proof is within intuitionistic logic. Otherwise, all proofs presented here are within minimal logic

(MIN)

2. Categorical subsets, complemented categorical subsets, and categorical partial functions

In $BST$ a set is usually equipped not only with a given equality i.e., with a given equivalence relation, but also with a given inequality relation. The primitive set of natural numbers $N$ has a given equality $=_{N}$ and inequality $\neq_{N}$ , which is a tight apartness relation.

Definition 2.1.
If $(X, =_{X})$ is a set and $⊥ : = 0 =_{N} 1$ , let the following formulas with respect to a relation $x \neq_{X} y$ :

( ${Ineq}_{1}$ ) $\forall_{x, y \in X} (x =_{X} y & x \neq_{X} y \Rightarrow ⊥)$ ,

( ${Ineq}_{2}$ ) $\forall_{x, x^{'}, y, y^{'} \in X} (x =_{X} x^{'} & y =_{X} y^{'} & x \neq_{X} y \Rightarrow x^{'} \neq_{X} y^{'})$ ,

( ${Ineq}_{3}$ ) $\forall_{x, y \in X} (\neg (x \neq_{X} y) \Rightarrow x =_{X} y)$ ,

( ${Ineq}_{4}$ ) $\forall_{x, y \in X} (x \neq_{X} y \Rightarrow y \neq_{X} x)$ ,

( ${Ineq}_{5}$ ) $\forall_{x, y \in X} (x \neq_{X} y \Rightarrow \forall_{z \in X} (z \neq_{X} x \lor z \neq_{X} y))$ ,

( ${Ineq}_{6}$ ) $\forall_{x, y \in X} (x =_{X} y \lor x \neq_{X} y)$ .

If ${Ineq}_{1}$ is satisfied, we call $\neq_{X}$ an inequality on X, and the structure $X : = (X, =_{X}, \neq_{X})$ a set with an inequality. If $({Ineq}_{6})$ is satisfied, then $X$ is called discrete. An inequality is called extensional, if $({Ineq}_{2})$ holds, and it is called tight, if $({Ineq}_{3})$ is satisfied. An inequality satisfying $({Ineq}_{4})$ and $({Ineq}_{5})$ is called an apartness relation on8
⁸
An apartness relation $\neq_{X}$ on a set $(X, =_{X})$ is always extensional.

X. If $Y : = (Y, =_{Y}, \neq_{Y})$ is a set with inequality, a function $f : X \to Y$ is strongly extensional, if $f (x) \neq_{Y} f (x^{'}) \Rightarrow x \neq_{X} x^{'}$ , for every $x, x^{'} \in X$ . Let $X : = (X, =_{X}, \neq_{X})$ and $Y : = (Y, =_{Y}, \neq_{Y})$ be sets with inequalities. The canonical inequalities on the product $X \times Y$ and the function space9
⁹
If X, Y are totalities an assignment routine f from X to Y is denoted by $f : X ⇝ Y$ , and it is a method, or an algorithm, according to which a term of set Y is assigned to a given term of set X. If X, Y are sets, $f : X ⇝ Y$ is a function, if it respects their equalities. A function is an embedding, if it is an injection.

$F (X, Y)$ are given, respectively, by $\begin{array}{c} (x, y) \neq_{X \times Y} (x^{'}, y^{'}) : \Leftrightarrow x \neq_{X} x^{'} \lor y \neq_{Y} y^{'}, \\ f \neq_{F (X, Y)} g : \Leftrightarrow \exists_{x \in X} [f (x) \neq_{Y} g (x)] . \end{array}$

The projections ${pr}_{X}$ , ${pr}_{Y}$ associated to $X \times Y$ are strongly extensional functions. It is not possible to give examples of non strongly extensional functions, although we cannot accept in $BISH$ that all functions are strongly extensional. E.g., the strong extensionality of all functions from a metric space to itself is equivalent to Markov’s principle (see [15], p. 40). Even to show that a constant function between sets with an inequality is strongly extensional, one needs intuitionistic, and not minimal, logic.
Definition 2.2 (Categorical subsets).

A categorical subset of a set $(X, =_{X})$ is a pair $(A, i_{A}^{X})$ , where A is a set and $i_{A}^{X} : A ↪ X$ is an embedding of A into X. If $(A, i_{A}^{X})$ and $(B, i_{B}^{X})$ are categorical subsets of X, then A is a subset of B, in symbols $(A, i_{A}^{X}) \subseteq (B, i_{B}^{X})$ , or simpler $A \subseteq B$ , if there is $f : A \to B$ such that the following triangle commutes

In this case we use the notation $f : A \subseteq B$ . Usually we write A instead of $(A, i_{A}^{X})$ . The totality of the categorical subsets of X is the categorical powerset $P (X)$ of X, and it is equipped with the equality $(A, i_{A}^{X}) =_{P (X)} (B, i_{B}^{X}) : \Leftrightarrow A \subseteq B & B \subseteq A$ . If $f : A \subseteq B$ and $g : B \subseteq A$ , we write $(f, g) : A =_{P (X)} B$ . If $\neq_{X}$ is a given inequality on X, the canonical inequality on $(A, i_{A}^{X}) \subseteq X$ is defined by $a \neq_{A} a^{'} : \Leftrightarrow i_{A}^{X} (a) \neq_{X} i_{A}^{X} (a^{'})$ .

Since the membership condition for $P (X)$ requires quantification over the universe $V_{0}$ of (predicative) sets, the totality $P (X)$ is a proper class. Clearly, $(X, {id}_{X}) \subseteq X$ , and if $f : A \subseteq B$ , then f is an embedding. The embedding $i_{A}^{X}$ of $A \subseteq X$ is trivially a strongly extensional function, and if $X : = (X, =_{X}, \neq_{X})$ is discrete, then $A : = (A, =_{A}, i_{A}^{X}, \neq_{A})$ is discrete, and if $\neq_{X}$ is tight, then $\neq_{A}$ is tight. In $BST$ the separation scheme is used to define new totalities from given ones. If $(X, =_{X})$ is a set, and $P (x)$ is a bounded formula on X i.e., $P (x)$ does not involve quantification over proper classes, the totality $X_{P}$ is defined by the membership condition $x \in X_{P} : \Leftrightarrow x \in X & P (x)$ . Its equality is inherited either from $=_{X}$ , or it is defined anew.10

¹⁰
The totality $A \cap B$ in Definition 2.5 is defined by separation on $A \times B$ but its equality is not inherited from $=_{A \times B}$ .

We use the standard notation

\begin{matrix} X_{P} : = {x \in X | P (x)} . \end{matrix}

In standard

BST

there is only one primitive set with an inequality, the natural numbers

N : = (N, =_{N}, \neq_{N})

. The set of Boolean-values can be defined either by separation on

N

, or as a new primitive set (as in

MLTT

). In this section we follow the latter option, as we want to work with categorical subsets as much as possible.11

¹¹

The only extensional subset (see Definition 4.1) used in this section is the diagonal of a set in Definition 2.8.

Definition 2.3 (Booleans and the unit set).

Let the primitive set of Boolean-values $2 : = (2, =_{2}, \neq_{2})$ , where for simplicity the elements of 2 are denoted by 0 and 1, and $=_{2}, \neq_{2}$ are the obvious equality and inequality relations on 2. We also write $2 = : {0, 1}$ . Moreover, let the primitive unit set $1 : = (1, =_{1}, \neq_{1})$ , with a given element ∗, equipped with the obvious equality and $* \neq_{1} * : \Leftrightarrow ⊥$ . We also write $1 = : {*}$ . Let ${1} : = (1, o) \subseteq 2$ , where $o : 1 ↪ 2$ is defined by $o (*) : = 1$ , and let ${0} : = (1, z) \subseteq 2$ , where $z : 1 ↪ 2$ is defined by $z (*) : = 0$ .

Definition 2.4 (Categorical empty subset).

If $x_{0} \in X$ , the totality $\emptyset_{X}$ is defined by $z \in \emptyset_{X} : \Leftrightarrow x_{0} \in X & 0 =_{N} 1$ . If $i_{\emptyset}^{X} : \emptyset_{X} ⇝ X$ is defined by $i (z) : = x_{0}$ , for every $z \in \emptyset_{X}$ , let $z =_{\emptyset_{X}} w : \Leftrightarrow i (z) =_{X} i (w) : \Leftrightarrow x_{0} =_{X} x_{0}$ .

One can show that $=_{\emptyset_{X}}$ is an equality on $\emptyset_{X}$ , and hence $\emptyset_{X}$ can be considered to be a set, and that $i_{\emptyset}^{X}$ is an embedding of $\emptyset_{X}$ into X. In contrast to the recursion rule of the empty type in Martin-Löf Type Theory $(MLTT)$ , in order to define an assignment routine $f : \emptyset_{X} ⇝ A$ , we need an element of A. If $A \subseteq X$ is inhabited, one needs Ex falso to show $\emptyset_{X} \subseteq A$ . Moreover, $\emptyset_{A} \subseteq X$ , but no explicit functions can be defined between $\emptyset_{A}$ and $\emptyset_{X}$ .

Definition 2.5.
Let $(A, i_{A}^{X}), (B, i_{B}^{X}) \subseteq X$ . Their union $A \cup B$ is the totality defined by $z \in A \cup B : \Leftrightarrow z \in A \lor z \in B$ , equipped with the non-dependent assignment routine12
¹²
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. At this point it doesn’t make sense to say that z is both in A and in B, and $i_{A \cup B}^{X} (z)$ is well-defined. If $(a, b)$ is in the intersection $A \cap B$ , as this is defined next, then $i_{A \cup B}^{X} (a) : = i_{A}^{X} (a) =_{X} i_{B}^{X} (b) = : i_{A \cup B}^{X} (b)$ .

$i_{A \cup B}^{X} : A \cup B ⇝ X$ , defined by $\begin{matrix} i_{A \cup B}^{X} (z) : = \{\begin{array}{ll} i_{A}^{X} (z), & z \in A \\ i_{B}^{X} (z), & z \in B . \end{array} \end{matrix}$ If $z, w \in A \cup B$ , let $z =_{A \cup B} w : \Leftrightarrow i_{A \cup B}^{X} (z) =_{X} i_{A \cup B}^{X} (w)$ . The intersection $A \cap B$ is the totality $\begin{matrix} A \cap B : = {(a, b) \in A \times B | i_{A}^{X} (a) =_{X} i_{B}^{X} (b)} \end{matrix}$

Let $i_{A \cap B}^{X} : A \cap B ⇝ X$ , where $i_{A \cap B}^{X} (a, b) : = i_{A}^{X} (a)$ , for every $(a, b) \in A \cap B$ . If $(a, b), (a^{'}, b^{'}) \in A \cap B$ , let $(a, b) =_{A \cap B} (a^{'}, b^{'}) : \Leftrightarrow i_{A \cap B}^{X} (a, b) =_{X} i_{A \cap B}^{X} (a^{'}, b^{'}) : \Leftrightarrow i_{A}^{X} (a) =_{X} i_{A}^{X} (a^{'})$ .

Clearly, $=_{A \cup B}$ is an equality on $A \cup B$ , $i_{A \cup B}^{X}$ is an embedding of $A \cup B$ into X, and the pair $(A \cup B, i_{A \cup B}^{X})$ is a subset of X. Similarly, $=_{A \cap B}$ is an equality on $A \cap B$ , $i_{A \cap B}^{X}$ is an embedding of $A \cap B$ into X, and the pair $(A \cap B, i_{A \cap B}^{X})$ is a subset of X. Notice that the definition of $A \cap B$ is the standard pullback construction. All standard properties of union and intersection of subsets hold, except from those involving the categorical empty subset. Even if A is an inhabited subset of X, and if $a_{0} \in A$ , then one needs the equality $i_{A}^{X} (a_{0}) = x_{0}$ , where $x_{0}$ is the given inhabitand of X, to show that $\emptyset_{X} \cup A \subseteq A$ . The same equality is required to show that $\emptyset_{X} \cap A =_{P (X)} A$ . Consequently, standard properties of the classical calculus of $(P (X), \cup, \cap)$ do not go through in Bishop’s categorical approach to the powerset.
Definition 2.6.
Let X, Y be sets, $(A, i_{A}^{X}), (C, i_{C}^{X}) \subseteq X$ , $e : (A, i_{A}^{X}) \subseteq (C, i_{C}^{X})$ , $f : C \to Y$ , and $(B, i_{B}^{Y}) \subseteq Y$ . The restriction $f_{|_{A}}$ of f to A is the function $f_{|_{A}} : = f \circ e$

The image $f (A)$ of A under f is the pair $f (A) : = (A, f_{|_{A}})$ , $a =_{f (A)} a^{'} : \Leftrightarrow f_{|_{A}} (a) =_{Y} f_{|_{A}} (a^{'})$ , for every $a, a^{'} \in A$ . We denote ${f (a) | a \in A} : = f (A)$ . The pre-image $f^{- 1} (B)$ of B under f is the set $\begin{matrix} f^{- 1} (B) : = {(c, b) \in C \times B | f (c) =_{Y} i_{B}^{Y} (b)} . \end{matrix}$ Let $i_{f^{- 1} (B)}^{C} : f^{- 1} (B) ↪ C$ , defined by $i_{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$ . The product of $(A, i_{A}^{X})$ and $(B, i_{B}^{Y})$ is the pair $(A \times B, i_{A \times B}^{X \times Y})$ , where $i_{A \times B}^{X \times Y} : A \times B ⇝ X \times Y$ is defined by $i_{A \times B}^{X \times Y} (a, b) : = (i_{A}^{X} (a), i_{B}^{Y} (b))$ , for every $(a, b) \in A \times B$ . Moreover, $(a, b) =_{A \times B} (a^{'}, b^{'}) : \Leftrightarrow i_{A \times B}^{X \times Y} (a, b) =_{X \times Y} i_{A \times B}^{X \times Y} (a^{'}, b^{'})$ .

Clearly, the restriction $f_{|_{A}}$ of $f : X \to Y$ to $(A, i_{A}^{X}) \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}) =_{P (X)} (B, i_{B}^{X}) \Rightarrow i_{A}^{X} (A) =_{P (X)} i_{B}^{X} (B)$ , since, if $(f, g) : (A, i_{A}^{X}) =_{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. A family of categorical subsets of a set X indexed by some set I is an assignment routine $λ_{0} : I ⇝ P (X)$ that behaves like a function i.e., if $i =_{I} j$ , then $λ_{0} (i) =_{P (X)} λ_{0} (j)$ . The following definition is a formulation of this rough description that reveals the witnesses of the equality $λ_{0} (i) =_{P (X)} λ_{0} (j)$ . This is done “internally”, through the embeddings of the subsets into X. The equality $λ_{0} (i) =_{V_{0}} λ_{0} (j)$ , which is defined “externally” through the transport maps (see [34], Definition 3.1), follows, and a family of categorical subsets is also a family of sets. For details we refer to [32,34].
Definition 2.7.
Let I be a set and $λ_{0} : I ⇝ V_{0}$ . A dependent operation over $λ_{0}$ , in symbols $Φ : ⋏_{i \in I} λ_{0} (i)$ assigns to each $i \in I$ an element $Φ (i) : = Φ_{i} \in λ_{0} (i)$ . We denote by $A (I, λ_{0})$ the totality of dependent operations over $λ_{0}$ together with the equality $Φ =_{A (I, λ_{0})} Ψ : \Leftrightarrow \forall_{i \in I} (Φ_{i} =_{λ_{0} (i)} Ψ_{i})$ .
Definition 2.8.
Let sets $(X, =_{X})$ and $(I, =_{I})$ and let $D (I) : = {(i, j) \in I \times I | i =_{I} j}$ the diagonal of I, equipped with the equality inherited from $=_{I \times I}$ . A family of subsets of X indexed by I is a triplet $Λ (X) : = (λ_{0}, E, λ_{1})$ , where $\begin{array}{c} λ_{0} : I ⇝ V_{0}, E : ⋏_{i \in I} F (λ_{0} (i), X), E (i) : = E_{i}; i \in I, \\ λ_{1} : ⋏_{(i, j) \in D (I)} F (λ_{0} (i), λ_{0} (j)), λ_{1} (i, j) : = λ_{i j}; (i, j) \in D (I), \end{array}$ such that the following conditions hold:

(a) For every $i \in I$ , the function $E_{i} : λ_{0} (i) \to X$ is an embedding.

(b) For every $i \in I$ , we have that $λ_{i i} =_{F (λ_{0} (i), λ_{0} (i))} {id}_{λ_{0} (i)}$ .

(c) For every $(i, j) \in D (I)$ we have that $E_{i} =_{F (λ_{0} (i), X)} E_{j} \circ λ_{i j}$ We call a pair $A_{i} : = (λ_{0} (i), E_{i})$ an element of $Λ (X)$ . If $(A, i_{A}) \in P (X)$ , the constant I-family of subsets A is the pair $C^{A} (X) : = (λ_{0}^{A}, E^{A}, λ_{1}^{A})$ , where $λ_{0} (i) : = A$ , $E_{i}^{A} : = i_{A}^{X}$ , and $λ_{1} (i, j) : = {id}_{A}$ , for every $i \in I$ and $(i, j) \in D (I)$ , respectively. If $(A, i_{A}^{X}), (B, i_{B}^{X}) \subseteq X$ , the triplet $Λ^{2} (X) : = (λ_{0}^{2}, E, λ_{1}^{2})$ , where $λ_{0}^{2} (0) : = A$ and $λ_{0}^{2} (1) : = B$ , $E_{0} : = i_{A}^{X}$ and $E_{1} : = i_{B}^{X}$ , $λ_{1}^{2} (0, 0) : = {id}_{A}$ and $λ_{1}^{2} (1, 1) : = {id}_{B}$ .

The above definition of a family of subsets over an index-set I is a “proof-relevant” way of saying that the assignment routine $λ_{0} : I ⇝ V_{0}$ behaves like a function i.e., $i =_{I} j \Rightarrow λ_{0} (i) =_{P (X)} λ_{0} (j)$ , as $λ_{i j} : λ_{0} (i) \subseteq λ_{0} (j)$ and $λ_{j i} : λ_{0} (j) \subseteq λ_{0} (i)$ .
Definition 2.9.
The interior union, or the union of $Λ (X)$ is the totality $\sum_{i \in I} λ_{0} (i)$ , which we denote in this case by $⋃_{i \in I} λ_{0} (i)$ , with membership-condition $z \in ⋃_{i \in I} λ_{0} (i) : \Leftrightarrow \exists_{i \in I} \exists_{x \in λ_{0} (i)} (z : = (i, x))$ . Let $e : ⋃_{i \in I} λ_{0} (i) ⇝ X$ defined by $(i, x) \mapsto E_{i} (x)$ , for every $(i, x) \in ⋃_{i \in I} λ_{0} (i)$ , and let $(i, x) =_{⋃_{i \in I} λ_{0} (i)} (j, y) : \Leftrightarrow e (i, x) =_{X} e (j, y) : \Leftrightarrow E_{i} (x) =_{X} E_{j} (y)$ . If $\neq_{X}$ is an inequality on X, let $(i, x) \neq_{⋃_{i \in I} λ_{0} (i)} (j, y) : \Leftrightarrow E_{i} (x) \neq_{X} E_{j} (y)$ .

If $i_{0} \in I$ , the intersection $⋂_{i \in I} λ_{0} (i)$ of $Λ (X)$ is the totality defined by $\begin{matrix} Φ \in ⋂_{i \in I} λ_{0} (i) : \Leftrightarrow Φ \in A (I, λ_{0}) & \forall_{i, j \in I} (E_{i} (Φ_{i}) =_{X} E_{j} (Φ_{j})) . \end{matrix}$ Let $e : ⋂_{i \in I} λ_{0} (i) ⇝ X$ be defined by $e (Φ) : = E_{i_{0}} (Φ_{i_{0}})$ , for every $Φ \in ⋂_{i \in I} λ_{0} (i)$ , and $Φ =_{⋂_{i \in I} λ_{0} (i)} Θ : \Leftrightarrow e (Φ) =_{X} e (Θ) : \Leftrightarrow E_{i_{0}} (Φ_{i_{0}}) =_{X} E_{i_{0}} (Θ_{i_{0}})$ , If $\neq_{X}$ is a given inequality on X, let $Φ \neq_{⋂_{i \in I} λ_{0} (i)} Θ : \Leftrightarrow E_{i_{0}} (Φ_{i_{0}}) \neq_{X} E_{i_{0}} (Θ_{i_{0}})$ .

If $Λ^{2} (X)$ is the 2-family of subsets A, B of X, then $⋃_{i \in 2} λ_{0}^{2} (i) =_{P (X)} A \cup B$ and $⋂_{i \in 2} λ_{0}^{2} (i) =_{P (X)} A \cap B$ . All standard properties of union and intersection of families of categorical subsets hold, except from those involving $\emptyset_{X}$ . An inequality on a set X induces a positively defined notion of disjointness of subsets of X. The positive disjointness of categorical subsets of X induces the notion of a categorical 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.
Definition 2.10.
Let $X : = (X, =_{X}, \neq_{X})$ be a set with an inequality, and $(A, i_{A}^{X}), (B, i_{B}^{X}) \subseteq X$ . We say that A and B are disjoint with respect to $\neq_{X}$ , in symbols $A) (_{\neq_{X}} B$ , if $\forall_{a \in A} \forall_{b \in B} (i_{A}^{X} (a) \neq_{X} i_{B}^{X} (b))$ . If $\neq_{X}$ is clear from the context, we only write13
¹³
Our notation of disjoint subsets complements naturally Sambin’s notation of intersecting subsets $A ≬ B$ .

$A) (B$ . A complemented categorical subset of $X$ is a pair $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}) (A^{0}$ . We call $A^{1}$ the 1-component of $A$ and $A^{0}$ the 0-component of $A$ . If $Dom (A) : = A^{1} \cup A^{0}$ is the domain of $A$ , the characteristic function of $A$ is the operation $χ_{A} : Dom (A) ⇝ 2$ , where $\begin{matrix} χ_{A} (x) : = \{\begin{array}{ll} 1, & x \in A^{1} \\ 0, & x \in A^{0} . \end{array} \end{matrix}$ We call $A$ total, if $Dom (A) =_{P (X)} X$ , and inhabited $(coinhabited)$ , if $A^{1}$ $(A^{0})$ is inhabited. If $A$ , $B$ are complemented categorical subsets of X, let $A \subseteq B : \Leftrightarrow A^{1} \subseteq B^{1} & B^{0} \subseteq A^{0}$ . Let $P^{) (} (X)$ be their proper class, equipped with the equality $A =_{P^{) (} (X)} B : \Leftrightarrow A \subseteq B & B \subseteq A$ .

The following proposition is straightforward to show.
Proposition 2.11.
Let $X : = (X, =_{X}, \neq_{X})$ , $Y : = (Y, =_{Y}, \neq_{Y})$ be sets with an extensional inequality, let $f : X \to Y$ be strongly extensional, and let $g : X \to Y$ be an injection. 14
¹⁴
I.e., $x \neq_{X} x^{'} \Rightarrow f (x) \neq_{Y} f (x^{'})$ , for every $x, x^{'} \in X$ . Clearly, if f is an injection and $\neq_{X}$ is a tight apartness, then f is an embedding.

If $B : = (B^{1}, B^{0}) \in P^{) (} (Y)$ , then $f^{- 1} (B) : = (f^{- 1} (B^{1}), f^{- 1} (B^{0})) \in P^{) (} (X)$ .

The substitution class-assignment routine $f^{} : P^{) (} (Y) ⇝ P^{) (} (X)$ , $B \mapsto f^{- 1} (B)$ , is a monotone class-function.*

If $A : = (A^{1}, A^{0}) \in P^{) (} (X)$ , then $g (A) : = (g (A^{1}), g (A^{0})) \in P^{) (} (Y)$ .

The class-assignment routine $g_{} : P^{) (} (X) ⇝ P^{) (} (Y)$ , $A \mapsto g (A)$ , is a monotone class-function.*

Definition 2.12.
A categorical partial function from X to Y is a triplet $f_{A} : = (A, i_{A}^{X}, f_{A})$ , where $(A, i_{A}^{X}) \subseteq X$ , and $f_{A} \in F (A, Y)$ . We call $f_{A}$ total, if $dom (f_{A}) : = A =_{P (X)} X$ . Let $f_{A} ⪯ f_{B}$ , if there is an embedding $e_{A B} : A ↪ B$ such that the following triangles commute In this case we write $e_{A B} : f_{A} ⪯ f_{B}$ . The categorical partial function space $F (X, Y)$ is equipped with the equality $f_{A} =_{F (X, Y)} f_{B} : \Leftrightarrow f_{A} ⪯ f_{B} & f_{B} ⪯ f_{A}$ . If X, Y are equipped with inequalities $\neq_{X}$ , $\neq_{Y}$ , respectively, let $F^{se} (X, 2)$ be the totality15
¹⁵
As the membership condition of $F (X, Y)$ requires quantification over the universe $V_{0}$ , the totalities $F (X, Y)$ and $F^{se} (X, Y)$ are proper classes.

of strongly extensional, partial functions from X to Y. Accordingly, $(F^{se} (X, 2)) F (X, 2)$ is the proper class of (strongly extensional) categorical, Boolean-valued, partial functions on X.

Clearly, if $A \in P^{) (} (X)$ , then $(A^{1} \cup A^{0}, i_{A^{1} \cup A^{0}}^{X}, χ_{A}) \in F (X, 2)$ . If $f, g \in F (X, 2)$ , let $\sim f : = 1 - f$ , and $f \lor g : = max {f, g}$ , $f \cdot g : = f \land g : = min {f, g}$ on $dom (f) \cap dom (g)$ .
Proposition 2.13.
If $A \in P^{) (} (X)$ , then $χ_{A}$ is a strongly extensional, Boolean-valued, partial function on X.
Proof.
Let $z, w \in A^{1} \cup A^{0}$ with $χ_{A} (z) \neq_{2} χ_{A} (w)$ . Let $χ_{A} (z) : = 1$ and $χ_{A} (w) : = 0$ . In this case $z \in A^{1}$ , $w \in A^{0}$ . Since $A^{1}) (A^{0}$ , we get $i_{A^{1}}^{X} (z) \neq_{X} i_{A^{0}}^{X} (w) \Leftrightarrow : z \neq_{A^{1} \cup A^{0}} w$ . If $χ_{A} (z) : = 0$ and $χ_{A} (w) : = 1$ , we work similarly. □

Set-indexed families of (categorical) complemented subsets and of (categorical) partial functions are defined similarly to Definition 2.8, and are studied in [32], Sections 4.8 and 4.9. Notice that in the formulation of the next fact we refer to assignment routines defined on proper classes, and we use Definition 2.6.
Proposition 2.14.
If $X : = (X, =_{X}, \neq_{X})$ is a set with an inequality, let us consider the assignment routines $\begin{array}{c} χ : P^{) (} (X) ⇝ F^{se} (X, 2) & δ : F^{se} (X, 2) ⇝ P^{) (} (X), \\ A \mapsto χ (A) f_{A} \mapsto δ (f_{A}) : = (δ^{1} (f_{A}), δ^{0} (f_{A})), \end{array}$ where $\begin{array}{c} δ^{1} (f_{A}) : = f^{- 1} ({1}) : = {(a, ) \in A \times 1 | f_{A} (a) =_{2} o () : = 1}, \\ δ^{0} (f_{A}) : = f^{- 1} ({0}) : = {(a, ) \in A \times 1 | f_{A} (a) =_{2} z () : = 0}, \end{array}$ for every $A : = (A^{1}, i_{A^{1}}^{X}, A^{0}, i_{A^{0}}^{X}) \in P^{) (} (X)$ and every $f_{A} : = (A, i_{A}^{X}, f_{A}^{2}) \in F^{se} (X, 2)$ . Then χ, δ are well-defined proper-class-functions, which are inverse to each other.
Proof.
By Proposition 2.13χ is well-defined. If $A, B \in P^{) (} (X)$ , $(e_{1}, j_{1}) : A^{1} =_{P (X)} B^{1}$ and $(e_{0}, j_{0}) : A^{0} =_{P (X)} B^{0}$ , it is straightforward to show that $(e, j) : χ_{A} =_{F^{se} (X, 2)} χ_{B}$ where $e : A^{1} \cup A^{0} \to B^{1} \cup B^{0}$ and $j : B^{1} \cup B^{0} \to A^{1} \cup A^{0}$ are defined by $\begin{matrix} e (z) : = \{\begin{array}{ll} e_{1} (z), & z \in A^{1} \\ e_{0} (z), & z \in A^{0} \end{array}, j (w) : = \{\begin{array}{ll} j_{1} (w), & w \in B^{1} \\ j_{0} (w), & w \in B^{0} . \end{array} \end{matrix}$ To show $δ (f_{A}) \in P^{) (} (X)$ , let $(a, ) \in δ^{1} (f_{A}^{2})$ and $(b, ) \in δ^{0} (f_{A}^{2})$ . As $f_{A}^{2} (a) =_{2} 1 \neq_{2} 0 =_{2} f_{A}^{2} (b)$ , by the strong extensionality of $f_{A}^{2}$ , and according to the canonical inequality on $(A, i_{A}^{X})$ , we get $a \neq_{A} b : \Leftrightarrow i_{A}^{X} (a) \neq_{X} i_{A}^{X} (b)$ . If $(A, i_{A}^{X}, f_{A}^{2}) =_{F^{se} (X, 2)} (B, i_{B}^{X}, f_{B}^{2})$ , then commutativities $(#_{1})$ and $(#_{2})$ of the following outer diagrams $(A, B, 2)$ imply that ${(e_{A B})}_{| δ^{1} (f_{A}^{2})} : δ^{1} (f_{A}^{2}) \to δ^{1} (f_{B}^{2})$ and ${(e_{B A})}_{| δ^{1} (f_{B}^{2})} : δ^{0} (f_{A}^{2}) \to δ^{0} (f_{B}^{2})$ are well-defined, and the commutativities $(#_{3})$ , $(#_{4})$ of the above inner diagrams $(A, B, X)$ imply the commutativity of the following diagrams The equalities $δ (χ (A)) =_{P^{) (} (X)} A$ and $χ (δ (f_{A})) =_{F^{se} (X, 2)} f_{A}$ follow easily. □

The use of $F^{se} (X, 2)$ , and not of $F (X, 2)$ , is crucial to the well-definability of δ.
3. The two algebras of complemented categorical subsets

In BMT, what we call here, the first algebra $B_{1} (X)$ of complemented categorical subsets is considered, while in $BCMT$ , the second algebra $B_{2} (X)$ is considered, which has a more “linear” behavior (see [43,49]). All operations between categorical subsets in this section are determined by the corresponding definitions of the previous one.

Definition 3.1 (The first algebra).

If $A, B \in P^{) (} (X)$ and $C \in P^{) (} (Y)$ , let the following operations on them: $\begin{array}{c} A \cup B : = (A^{1} \cup B^{1}, A^{0} \cap B^{0}), A \cap B : = (A^{1} \cap B^{1}, A^{0} \cup B^{0}), \\ - A : = (A^{0}, A^{1}), A \sim B : = A \cap (- B), \\ A * C : = (A^{1} \times C^{1}, [A^{0} \times Y] \cup [X \times C^{0}]) . \end{array}$ If ${(λ (i))}_{i \in I}$ is an I-family of complemented subsets of X i.e., $λ (i) : = (λ^{1} (i), λ^{0} (i)) \in P^{) (} (X)$ , for every $i \in I$ , let $\begin{matrix} ⋃_{i \in I} λ (i) : = (⋃_{i \in I} λ^{1} (i), ⋂_{i \in I} λ^{0} (i)) \in P^{) (} (X), ⋂_{i \in I} λ (i) : = (⋂_{i \in I} λ^{1} (i), ⋃_{i \in I} λ^{0} (i)) \in P^{) (} (X) . \end{matrix}$

Within (INT), if $A$ is total, then $(A \cup - A) \cap B =_{P^{) (} (X)} B$ . Clearly, $A \subseteq B \Leftrightarrow A \cap B = A$ . The following proposition is straightforward to prove.

Proposition 3.2.
The first algebra $B_{1} (X) : = (P^{) (} (X), \cup, \cap, -)$ is a distributive lattice such that $- (- A) = A$ , for every $A \in P^{) (} (X)$ . If I is a set and ${(λ (i))}_{i \in I}$ is an I-family of complemented subsets of X, the following hold:
$- ⋃_{i \in I} λ (i) =_{P^{) (} (X)} ⋂_{i \in I} (- λ (i))$ .

$(A \cup - A) \cap (A \cup ⋂_{i \in I} λ (i)) =_{P^{) (} (X)} (A \cup - A) \cap [⋂_{i \in I} (A \cup λ (i))]$ .

The dual to condition (i) follows immediately. Condition (ii) is the constructive counterpart to distributivity:16
¹⁶
The dual to condition (ii), which is equivalent to it, is the equality $\begin{matrix} (A \cap - A) \cup (A \cap ⋃_{i \in I} λ (i)) =_{P^{) (} (X)} (A \cap - A) \cup [⋃_{i \in I} (A \cap λ (i))], \end{matrix}$ and it is the constructive counterpart to $A \cap ⋃_{i \in I} λ (i) =_{P^{) (} (X)} ⋃_{i \in I} (A \cap λ (i))$ .

$\begin{matrix} (D_{I}) A \cup ⋂_{i \in I} λ (i) =_{P^{) (} (X)} ⋂_{i \in I} (A \cup λ (i)) . \end{matrix}$ In Proposition 5.2 we show that $(D_{N})$ cannot be accepted constructively, as it implies $LPO$ , a “taboo” of constructive mathematics, according to which every Boolean-valued sequence is constant 0, or it takes the value 1 on some $n \in N$ . We do not prove this in the proof-relevant framework of categorical subsets, but in the simpler framework of extensional subsets. As the only operation involved is that of complementation, which as we can see in Definition 3.4 is common in both algebras, Proposition 2.14 pertains to both algebras of complemented subsets. Clearly, $δ (\sim f) =_{P^{) (} (X)} - δ (f)$ and $χ_{- A} =_{F (X, 2)} \sim χ_{A}$ , where $f \in F^{se} (X, 2)$ and $A \in P^{) (} (X)$ , while in general the operations $\cup, \cap$ of $B_{1} (X)$ are not preserved by the class-functions χ and δ of Proposition 2.14. The following facts are straightforward to show.
Proposition 3.3.
Let $A, B \in P^{) (} (X)$ and $f, g \in F^{se} (X, 2)$ .
If $A$ is total, then $χ_{A}$ is total, and if $f$ is total, then $δ (f)$ is total.

If $A$ , $B$ are total, then $A \cup B, A \cap B$ are total, and $χ_{A \cup B} =_{F (X, 2)} χ_{A} \lor χ_{B}$ , $χ_{A \cap B} =_{F (X, 2)} χ_{A} \land χ_{B}$ .

If $f_{A}$ , $f_{B}$ are total, then $f_{A} \lor f_{B}$ , $f_{A} \land f_{B}$ are total, and $δ (f_{A}) \cup δ (f_{B}) = δ (f_{A} \lor f_{B})$ , $δ (f_{A}) \cap δ (f_{B}) = δ (f_{A} \land f_{B})$ .

Definition 3.4 (The second algebra).

If $A, B \in P^{) (} (X)$ and $C \in P^{) (} (Y)$ , let the following operations on them: $\begin{array}{c} A ⋎ B : = ([A^{1} \cap B^{1}] \cup [A^{1} \cap B^{0}] \cup [A^{0} \cap B^{1}], A^{0} \cap B^{0}), \\ A ⋏ B : = (A^{1} \cap B^{1}, [A^{1} \cap B^{0}] \cup [A^{0} \cap B^{1}] \cup [A^{0} \cap B^{0}]), \\ - A : = (A^{0}, A^{1}), A ∽ B : = A ⋏ (- B), \\ A ⊛ C : = (A^{1} \times C^{1}, [A^{1} \times C^{0}] \cup [A^{0} \times C^{1}] \cup [A^{0} \times C^{0}]) . \end{array}$ More generally, if ${(λ (i))}_{i \in I}$ is an I-family of complemented subsets of X, let $\begin{array}{c} ⋎_{i \in I} λ (i) : = ([⋂_{i \in I} (λ^{1} (i) \cup λ^{0} (i))] \cap [⋃_{i \in I} λ^{1} (i)], ⋂_{i \in I} λ^{0} (i)), \\ ⋏_{i \in I} λ (i) : = (⋂_{i \in I} λ^{1} (i), [⋂_{i \in I} (λ^{1} (i) \cup λ^{0} (i))] \cap [⋃_{i \in I} λ^{0} (i)]) . \end{array}$

Proposition 3.5.
The second algebra $B_{2} (X) : = (P^{) (} (X), ⋏, ⋎, -)$ satisfies the above properties of $B_{1} (X)$ , except the absorption equalities 17
¹⁷
In [4], p. 74, Bishop and Bridges mention that $B_{2} (X)$ satisfies “all the usual finite algebraic laws that do not involve the operation of set complementation”. In [14], p. 695, Coquand and Palmgren rightly notice that $B_{2} (X)$ does not satisfy the absorption equalities.

$(A ⋏ B) ⋎ A = A$ and $(A ⋎ B) ⋏ A = A$ .

Using an argument similar to that found in the proof of Proposition 5.2(i), the corresponding distributivity $(D_{N})$ for $B_{2} (X)$ implies $LPO$ . Although $B_{2} (X)$ is not a lattice, its crucial advantage over $B_{1} (X)$ , and the main reason for its introduction by Bishop and Cheng, is that ⋎ and ⋏ are preserved by the proper class-functions χ and δ. Proposition 3.6.
Let $A, B \in P^{) (} (X)$ , and $f, g \in F^{se} (X, 2)$ .
$χ_{A ⋎ B} =_{F^{se} (X, 2)} χ_{A} \lor χ_{B}$ , $χ_{A ⋏ B} =_{F^{se} (X, 2)} χ_{A} \land χ_{B}$ .

$χ_{- A} =_{F^{se} (X, 2)} 1 - χ_{A}$ and $χ_{A ∽ B} =_{F^{se} (X, 2)} χ_{A} (1 - χ_{B})$ .

$δ (f_{A}) ⋎ δ (f_{B}) =_{P^{) (} (X)} δ (f_{A} \lor f_{B})$ and $δ (f_{A}) ⋏ δ (f_{B}) =_{P^{) (} (X)} δ (f_{A} \land f_{B})$ .

$δ (f_{A} \sim f_{B}) =_{P^{) (} (X)} δ (f_{A}) ∽ δ (f_{B})$ .

$χ_{A ⊛ B} (x, y) =_{2} χ_{A} (x) \cdot χ_{B} (y)$ .

Proof.
We show only $χ_{A ⋏ B} =_{F (X, 2)} χ_{A} \land χ_{B}$ . By definition $\begin{matrix} χ_{A} \land χ_{B} : = (Dom (A) \cap Dom (B), i_{Dom (A) \cap Dom (B)}^{X}, {(χ_{A} \land χ_{B})}_{Dom (A) \cap Dom (B)}^{2}), \end{matrix}$ where ${(χ_{A} \land χ_{B})}_{Dom (A) \cap Dom (B)}^{2} (u, w) : = χ_{A} (u) \land χ_{B} (w)$ , for every $(u, w) \in Dom (A) \cap Dom (B)$ . By definition $\begin{matrix} χ_{A ⋏ B} : = (Dom (A ⋏ B), i_{Dom (A ⋏ B)}^{X}, {(χ_{A ⋏ B})}_{Dom (A ⋏ B)}^{2}) . \end{matrix}$

As $Dom (A ⋏ B) =_{P (X)} Dom (A) \cap Dom (B)$ , if $(f, g) : Dom (A ⋏ B) =_{P (X)} Dom (A) \cap Dom (B)$ , the above outer diagram also commutes and hence the two partial functions are equal in $F^{se} (X, 2)$ . □

4. Extensional subsets, complemented extensional subsets, and extensional partial functions

Definition 4.1 (Extensional subsets).

A bounded formula $P (x)$ , where x is a variable of set $(X, =_{X})$ , is an extensional property18

¹⁸
Notice that in $MLTT$ a property on a type X is described as a type family $P : X \to U$ over X, where $U$ is a universe and $X : U$ , and it is always extensional through the corresponding transport-term (see [50], Section 2.3).

on X, if

\begin{matrix} \forall_{x, y \in X} ([x =_{X} y & P (x)] \Rightarrow P (y)) . \end{matrix}

The totality

X_{P}

defined by the separation scheme is called an extensional subset of X, if its equality is inherited from

=_{X}

. If

\neq_{X}

is a given inequality on X, then the canonical inequality

\neq_{X_{P}}

X_{P}

is inherited from

\neq_{X}

. The totality of extensional subsets of X is denoted by

E (X)

. If

X_{P}, X_{Q} \in E (X)

, let

X_{P} ⊑ X_{Q} : \Leftrightarrow \forall_{x \in X} (P (x) \Rightarrow Q (x))

and

X_{P} =_{E (X)} X_{Q} : \Leftrightarrow X_{P} ⊑ X_{Q} & X_{Q} ⊑ X_{P}

. We may avoid writing the extensional property

P (x)

determining an extensional subset A of X, and in this case we write

A ⊑ X

. We define an inequality on

E (X)

as follows:

\begin{matrix} X_{P} \neq_{E (X)} X_{Q} : \Leftrightarrow \exists_{x \in X} ((P (x) \land \neg Q (x)) \lor (Q (x) \land \neg P (x))) . \end{matrix}

Notice that no quantification over the universe $V_{0}$ is required in the membership condition of $E (X)$ . In accordance to the fundamental distinction between judgments and propositions due to Martin-Löf, if $A, B \in E (X)$ , the inclusion $A ⊑ B$ is a formula that does not employ the membership symbol i.e., we do not say that for all $x \in X$ if $x \in A$ , then $x \in B$ , as such a definition would interpret the judgments $x \in A$ , $x \in B$ as formulas. If $A : = X_{P}$ and $B : = X_{Q}$ , we only need to prove $P (x) \Rightarrow Q (x)$ , for every $x \in X$ . There are non-extensional properties on a set i.e., bounded formulas $P (x)$ , where x is a variable of the set X, such that $P (x)$ and $x =_{X} y$ do not imply $P (y)$ . For example, let $n \in N$ , $q \in Q$ and $P_{q} (x)$ , where x is a variable of set $R$ , defined by $P_{q} (x) : = x_{n} =_{Q} q$ (a real number is defined in $BISH$ as a Cauchy sequence of rationals). If $y \in R$ such that $y =_{R} x$ , then it is not necessary that $y_{n} =_{Q} q$ , if $x_{n} =_{Q} q$ . A set X is an extensional subset of itself, in the sense that it is equal19

¹⁹

Two (predicative) sets X, Y are equal in $V_{0}$ if there is a bijection (or better a pair of bijections) between them, and in this case we write $X =_{V_{0}} Y$ . The bijection between X and $X_{=_{X}}$ is defined by the identity rule.

V_{0}

to the extensional subset

X_{=_{X}} : = {x \in X | x =_{X} x}

. The sets 1 and 2 that were considered primitive in Section 2 are defined here as extensional subsets of

N

\begin{matrix} 1 : = {x \in N | x =_{N} 1} : = {0}, 2 : = {x \in N | x =_{N} 0 \lor x =_{N} 1} : = {0, 1} \end{matrix}

As an equality

=_{X}

is extensional on

X \times X

, the diagonal

D (X, =_{X}) : = {(x, y) \in X \times X | x =_{X} y}

of X is an extensional subset of

X \times X

. In the following definition of the extensional empty subset of a set X we do not require X to be inhabited, as in Definition 2.4. We only need a given extensional inequality20

²⁰

In [9], p. 12, the empty subset of an arbitrary set X is defined as the set ${x \in X | x \notin X}$ . This definition treats the expression $\neg (x \in X)$ and hence the expression $x \in X$ as a formula, something which, following Martin-Löf, we avoid here.

\neq_{X}

associated to

(X, =_{X})

e.g., an apartness relation on X. A positive notion of an extensional subset being empty is also definable.

Definition 4.2 (Extensional empty subset).

If $X : = (X, =_{X}, \neq_{X})$ is a set with an extensional inequality, then we call $□ /_{X} : = {x \in X | x \neq_{X} x}$ the extensional empty subset of $X$ . We call $X_{P} \in E (X)$ empty, if $X_{P} ⊑ □ /_{X}$ .

Notice that within $INT$ the converse inclusion $□ /_{X} ⊑ X_{P}$ , for every extensional property $P (x)$ on X, holds. The extensionality of an equality $=_{X}$ implies that the inequality $\neg (x =_{X} y)$ on $(X, =_{X})$ is extensional, with associated empty subset the extensional subset ${x \in X | \neg (x =_{X} x)}$ . Although this definition employs negation, we can define inequalities on a set, and hence associated empty subsets, in a completely positive way.

Remark 4.3.
If $(X, a, =_{X}, \neq_{X})$ is an inhabited set with an inequality, where a is given element of X, then $□ /_{X} \neq_{E (X)} X$ .
Proof.
Clearly, $a =_{X} a$ and $\neg (a \neq_{X} a)$ , as $\neq_{X}$ satisfies $({Ineq}_{1})$ . □
Definition 4.4.
The canonical inequality on the set of reals $R$ is given by $a \neq_{R} b : \Leftrightarrow | a - b | > 0 \Leftrightarrow a > b \lor a < b$ , which is a special case of the canonical inequality on a metric space $(Z, d)$ , given by $z \neq_{(Z, d)} z^{'} : \Leftrightarrow d (z, z^{'}) > 0$ . If $(X, =_{X})$ is a set and $F ⊑ F (X)$ , the set of real-valued functions on X, the inequality on X induced by F is defined by $\begin{matrix} x \neq_{(X, F)} x^{'} : \Leftrightarrow \exists_{f \in F} (f (x) \neq_{R} f (x^{'})) . \end{matrix}$

The inequalities $a \neq_{R} b$ and $z \neq_{(Z, d)} z^{'}$ are tight apartness relations, while the inequality $x \neq_{(X, F)} y$ is an apartness relation, which is tight if and only if for every $x, x^{'} \in X$ $\begin{matrix} \forall_{f \in F} (f (x) =_{R} f (x^{'})) \Rightarrow x =_{X} x^{'} \end{matrix}$ No negation of some sort is used in the definition of the inequality $x \neq_{(X, F)} x^{'}$ , in the proof of its extensionality, and the last implication above can be seen as completely positive formulation of its tightness. If F is a Bishop topology of functions (see [31,33,34,37,41]), then $x \neq_{(X, F)} x^{'}$ is the canonical inequality of a Bishop space. The inequality $a \neq_{R} b$ is equivalent to such an inequality induced by functions, as $a \neq_{R} b \Leftrightarrow a \neq_{(R, Bic (R))} b$ , where $Bic (R)$ is the topology of Bishop-continuous functions of type $R \to R$ (see [31], Proposition 5.1.2.). By its extensionality, an inequality induced by functions provides a (fully) positive definition of the extensional empty subset, and of the extensional complement21
²¹
Notice that it is not clear how to define a complement of a categorical subset as a categorical subset, and an arbitrary categorical complemented subset determines such a complement through its 0-component.

$X_{P}^{\neq_{X}}$ of an extensional subset $X_{P}$ of X, where $\begin{matrix} X_{P}^{\neq_{X}} : = {x \in X | \forall_{y \in X_{P}} (x \neq_{X} y))} . \end{matrix}$ Clearly, if $\neq_{X}$ is an extensional inequality on X, property $[P^{\neq_{X}}] (x) : = \forall_{y \in X_{P}} (x \neq_{X} y))$ is extensional on $(X, =_{X})$ . Through this property we can define a stronger inequality on $E (X)$ as follows: $\begin{matrix} X_{P} {\overset{s}{\neq}}_{E (X)} X_{Q} : \Leftrightarrow \exists_{x \in X} ((P (x) \land [Q^{\neq_{X}}] (x)) \lor (Q (x) \land [P^{\neq_{X}}] (x))) . \end{matrix}$
Remark 4.5.
If $(X, a, =_{X}, \neq_{X})$ is an inhabited set with an inequality satisfying $({Ineq}_{5})$ , then $□ /_{X} {\overset{s}{\neq}}_{E (X)} X$ .
Proof.
Clearly, $a =_{X} a$ and if $x \neq_{X} x$ , then by cotransitivity we get $a \neq_{X} x$ . □

Next we define the extensional version of all the rest operations on categorical subsets found in Section 2. We use the symbols ⊔, ⊓ to denote the union and the intersection of extensional subsets as extensional subsets.
Definition 4.6.
Let $(X, =_{X})$ , $(Y, =_{Y})$ be sets, $A : = X_{P}$ , $B : = X_{Q} \in E (X)$ , $C : = Y_{R} \in E (Y)$ and $f : X \to Y$ . Let $\begin{array}{c} A ⊔ B : = {x \in X | P (x) \lor Q (x)}, A ⊓ B : = {x \in X | P (x) \land Q (x)}, \\ f [A] : = {y \in Y | \exists_{x \in X_{P}} (f (x) =_{Y} y)}, f^{- 1} [C] : = {x \in X | \exists_{y \in Y_{R}} (f (x) =_{Y} y)}, \\ A \times C : = {((x^{'}, y^{'}) \in X \times Y | \exists_{x \in X_{P}} \exists_{y \in Y_{R}} (x^{'} =_{X} x \land y^{'} =_{Y} y)} . \end{array}$ If $(I, =_{I})$ is a set, a family of extensional subsets of X indexed by I is an assignment routine $λ_{0} : I ⇝ V_{0}$ , such that for every $i, j \in I$ we have that $λ_{0} (i) : = X_{P_{i}}$ , where $P_{i} (x)$ is an extensional property on X, and if $i =_{I} j$ , then $X_{P_{i}} =_{E (X)} X_{P_{j}}$ . For simplicity we denote such a family by ${(X_{P_{i}})}_{i \in I}$ . Its union and intersection are given by $\begin{matrix} ⨆_{i \in I} λ_{0} (i) : = {x \in X | \exists_{i \in I} (P_{i} (x))}, ⊓_{i \in I} λ_{0} (i) : = {x \in X | \forall_{i \in I} (P_{i} (x))} . \end{matrix}$

Notice that the extensionality of $P (x)$ , $Q (x)$ and $R (y)$ , together with the preservation of equalities by a function, imply the extensionality of the bounded formulas $\begin{array}{c} (P \lor Q) (x) : = P (x) \lor Q (x), (P \land Q) (x) : = P (x) \land Q (x), \\ [f [P]] (y) : = \exists_{x \in X_{P}} (f (x) =_{Y} y), [f^{- 1} [R]] (x) : = \exists_{y \in Y_{R}} (f (x) =_{Y} y), \\ [P \times R] (x, y) : = \exists_{x^{'} \in X_{P}} \exists_{y^{'} \in Y_{R}} (x^{'} =_{X} x \land y^{'} =_{Y} y) . \end{array}$ Similarly, the extensionality of $P_{i} (x)$ , for every $i \in I$ , implies the extensionality of the bounded formulas $\begin{matrix} (⨆_{i \in I} P_{i}) (x) : = \exists_{i \in I} (P_{i} (x)), (⊓_{i \in I} P_{i}) (x) : = \forall_{i \in I} (P_{i} (x)) . \end{matrix}$
Proposition 4.7.
Let $X : = (X, =_{X}, \neq_{X})$ and $Y : = (Y, =_{Y}, \neq_{Y})$ be sets with an extensional inequality, and let $A : = X_{P} \in E (X)$ and $B : = Y_{Q} \in E (Y)$ .
$A ⊑ A ⊔ □ /_{X}$ and (INT) $A ⊔ □ /_{X} ⊑ A$ .

$A ⊓ □ /_{X} ⊑ □ /_{X}$ and (INT) $□ /_{X} ⊑ A ⊓ □ /_{X}$ .

$□ /_{X} ⊑ □ /_{X_{P}}$ and (INT) $□ /_{X_{P}} ⊑ □ /_{X}$ .

$□ /_{X} \times □ /_{Y} ⊑ □ /_{X \times Y}$ and (INT) $□ /_{X \times Y} ⊑ □ /_{X} \times □ /_{Y}$ .

$□ /_{X} \times B ⊑ □ /_{X \times Y}$ and (INT) $□ /_{X \times Y} ⊑ □ /_{X} \times B$ .

$A \times □ /_{Y} ⊑ □ /_{X \times Y}$ and (INT) $□ /_{X \times Y} ⊑ A \times □ /_{Y}$ .

Proof.
All inclusions that are within $INT$ require a trivial application of the Ex Falso rule. □

By Proposition 4.7(i) and (ii) we conclude that standard properties of the classical calculus of $(E (X), ⊔, ⊓)$ do go through in the Bishop (or in the Bridges-Richman) extensional approach to the powerset. Crucial to this “better” behavior of $E (X)$ than of $P (X)$ , which also affects the properties of the corresponding extensional versions of complemented subsets and Boolean-valued partial functions, is the use of the introduced here extensional empty subset $□ /_{X}$ . By Proposition 4.7(iii) all empty subsets formed by extensional subsets of a set X “collapse” to the extensional empty subset $□ /_{X}$ associated to $X$ . In [4], p. 69, Bishop and Bridges define two (categorical) 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 =_{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}$ , which in general cannot be defined explicitly. If A, B are extensional subsets of a set with inequality though, then a completely positive definition of disjoint subsets can be given22
²²
Exactly this definition is already given for arbitrary subsets of a set with inequality in [14], p. 694. For the properties of this inequality relation between subsets see [10].

in complete analogy to the definition of disjoint categorical subsets in Definition 2.10. Its relation to the property $A \cap B$ “is the void subset of X” is explained in Proposition 4.9.
Definition 4.8.
Let $X : = (X, =_{X}, \neq_{X})$ be a set with an inequality, and $A : = X_{P}$ , $B : = X_{Q} \in E (X)$ , we call A and B disjoint with respect to $\neq_{X}$ , in symbols $A {] [}_{\neq_{X}} B$ or simpler $A] [B$ , if $\forall_{x \in X_{P}} \forall_{x^{'} \in X_{Q}} (x \neq_{X} x^{'})$ . A complemented extensional subset of $X$ is a pair $A : = (A^{1}, A^{0})$ , where $A^{1} : = X_{P_{1}}$ , $A^{0} : = X_{P_{0}} \in E (X)$ such that $A^{1}] [A^{0}$ . Its characteristic function $χ_{A}$ is the function $χ_{A} : Dom (A) : = {x \in X | P_{1} (x) \lor P_{0} (x)} \to 2$ , defined by $\begin{matrix} χ_{A} (x) : = \{\begin{array}{ll} 1, & P_{1} (x) \\ 0, & P_{0} (x) . \end{array} \end{matrix}$ If $A$ , $B$ are complemented extensional subsets of X, let $A ⊑ B : \Leftrightarrow A^{1} ⊑ B^{1} & B^{0} ⊑ A^{0}$ . Let $E^{] [} (X)$ be their totality,23
²³
The totality $E^{] [} (X)$ can also be defined by separation as $E^{] [} (X) : = {(A^{1}, A^{0}) \in E (X) \times E (X) | A^{1}] [A^{0}}$ . The relation $R (A^{1}, A^{0}) : = A^{1}] [A^{0}$ is extensional on $E (X) \times E (X)$ , and as $E (X)$ is an impredicative set, $E (X) \times E (X)$ and $E^{] [} (X)$ are also impredicative sets.

equipped with the equality $A =_{E^{] [} (X)} B : \Leftrightarrow A ⊑ B & B ⊑ A$ . Let the inequality on $E^{] [} (X)$ defined by $\begin{matrix} A \neq_{E^{] [} (X)} B : \Leftrightarrow \exists_{x \in X} ((P_{1} (x) \land \neg Q_{1} (x)) \lor (Q_{0} (x) \land \neg P_{0} (x)) \lor (Q_{1} (x) \land \neg P_{1} (x)) \lor (P_{0} (x) \land \neg Q_{0} (x))) . \end{matrix}$ All the rest notions of complemented extensional subsets are defined as in Definition 2.10.

Clearly, if $A : = X_{P} \in E (X)$ , then the pair $μ A : = (A, A^{\neq_{X}})$ is in $E^{] [} (X)$ .
Proposition 4.9.
Let $X : = (X, =_{X}, \neq_{X})$ be a set with an extensional inequality, and $A : = X_{P}$ , $B : = X_{Q} \in E (X)$ .
If $A] [B$ , then $A ⊓ B ⊑ □ /_{X}$ i.e., $A ⊓ B$ is empty.

If $\neq_{X}$ is discrete and $A ⊓ B ⊑ □ /_{X}$ , then $A] [B$ .

Proof.
(i) By the definition of $A] [B$ follows that $\forall_{x \in X} (P (x) \land Q (x) \Rightarrow x \neq_{X} x)$ , which is the required inclusion.

(ii) If $P (a)$ and $Q (b)$ , for some $a, b \in X$ , then if $a =_{X} b$ , by the extensionality of $Q (x)$ we get $Q (a)$ . Since than $P (a) \land Q (a)$ , we get $a \neq_{X} a$ . Hence, by the discreteness of $\neq_{X}$ , we conclude that $a \neq_{X} b$ . □
Proposition 4.10.
Let $X : = (X, =_{X}, \neq_{X})$ , $Y : = (Y, =_{Y}, \neq_{Y})$ be sets with an extensional inequality, let $f : X \to Y$ be strongly extensional, and let $g : X \to Y$ be an injection.
If $B : = (B^{1}, B^{0}) \in E^{) (} (Y)$ , then $f^{- 1} [B] : = (f^{- 1} [B^{1}], f^{- 1} [B^{0}]) \in E^{) (} (X)$ .

The substitution class-assignment routine $f^{} : E^{) (} (Y) ⇝ E^{) (} (X)$ , $B \mapsto f^{- 1} [B]$ , is a monotone function.*

If $A : = (A^{1}, A^{0}) \in E^{) (} (X)$ , then $g [A] : = (g [A^{1}], g [A^{0}]) \in E^{) (} (Y)$ .

The class-assignment routine $g_{} : E^{) (} (X) ⇝ E^{) (} (Y)$ , $A \mapsto g [A]$ , is a monotone function.*

Definition 4.11.
An extensional partial function from X to Y is a (total) function $f_{A} : A \to Y$ , where $A : = X_{P} \in E (X)$ . We may also denote such a function by $f_{P} : X_{P} \to Y$ . We call $f_{A}$ total, if $dom (f_{A}) : = A =_{E (X)} X$ . If $B : = X_{Q} \in E (X)$ and $f_{Q} : X_{Q} \to Y$ let $\begin{matrix} f_{P} ⩽ f_{Q} : \Leftrightarrow X_{P} ⊑ X_{Q} \land \forall_{x \in X_{P}} (f_{P} (x) =_{Y} f_{Q} (y)) . \end{matrix}$ The extensional partial function space $F (X, Y)$ is equipped with the equality $f_{A} =_{F (X, Y)} f_{B} : \Leftrightarrow f_{A} ⩽ f_{B} & f_{B} ⩽ f_{A}$ . If $\neq_{X}$ , $\neq_{Y}$ are inequalities on X, Y, respectively, let $F^{se} (X, Y)$ be the totality of strongly extensional, extensional partial functions from X to Y. Accordingly, $(F^{se} (X, 2))$ $F (X, 2)$ is the totality of (strongly extensional) extensional, Boolean-valued, partial functions on X. If $\neq_{Y}$ is an inequality on Y, an inequality on $F (X, Y)$ is defined as follows: $\begin{matrix} f_{P} =_{F (X, Y)} f_{Q} : \Leftrightarrow X_{P} \neq_{E (X)} X_{Q} \lor [X_{P} =_{E (X)} X_{Q} \land \exists_{x \in X_{P}} (f_{P} (x) \neq_{Y} f_{Q} (x))] . \end{matrix}$

Clearly, if $A \in E^{] [} (X)$ , then $χ_{A} \in F (X, 2)$ . As in the case of categorical, Boolean-valued partial functions, we define $\sim f : = 1 - f$ , and $f \lor g : = max {f, g}$ , $f \cdot g : = f \land g : = min {f, g}$ on $dom (f) ⊓ dom (g)$ , for every $f, g \in F (X, 2)$ . Next follows the extensional version of Propositions 2.13 and 2.14.
Proposition 4.12.
Let $X : = (X, =_{X}, \neq_{X})$ be a set with an inequality. If $A \in E^{] [} (X)$ , then $χ_{A}$ is a strongly extensional, Boolean-valued, extensional partial function on X. Let the assignment routines $\begin{array}{c} χ^{e} : E^{) (} (X) ⇝ F^{se} (X, 2) & δ^{e} : F^{se} (X, 2) ⇝ E^{) (} (X), \\ A \mapsto χ (A) f_{A} \mapsto δ^{e} (f_{A}) : = (δ^{1} (f_{A}), δ^{0} (f_{A})), \end{array}$ where $\begin{matrix} δ^{1} (f_{A}) : = {a \in A | f_{A} (a) =_{2} 1}, δ^{0} (f_{A}) : = {a \in A | f_{A} (a) =_{2} 0}, \end{matrix}$ for every $A \in E^{] [} (X)$ and $f_{A} \in F^{se} (X, 2)$ . Then $χ^{e}$ , $δ^{e}$ are well-defined functions, which are inverse to each other.
Proof.
Let $a, b \in X$ such that $χ_{A} (a) \neq_{2} χ_{A} (b)$ , $P_{1} (a)$ and $P_{0} (b)$ . As $X_{P_{1}}] [X_{P_{0}}$ , we get $a \neq_{X} b$ . The proof that $χ^{e}$ , $δ^{e}$ are well-defined functions, which are inverse to each other, follows in a straightforward manner. □

Set-indexed families of complemented extensional subsets and extensional partial functions are defined similarly to Definition 4.6. These families are not studied in [32], where mainly the proof-relevant aspects of $BST$ are studied.
5. The two algebras of complemented extensional subsets

The two algebras of complemented extensional subsets are defined by replacing ∪, ⋃ and $\cap, ⋂$ with ⊔, ⨆ and ⊓, ⊓ in Definitions 3.1 and 3.4, respectively. All operations between extensional subsets that appear in this section are determined by the corresponding definitions in the previous section. For the first algebra of complemented extensional subsets $B_{1}^{e} (X) : = (E^{] [} (X), ⊔, ⊓, -)$ of X we have $\begin{array}{c} A ⊔ B : = (A^{1} ⊔ B^{1}, A^{0} ⊓ B^{0}), ⨆_{i \in I} λ (i) : = (⨆_{i \in I} λ^{1} (i), ⊓_{i \in I} λ^{0} (i)), \\ A ⊓ B : = (A^{1} ⊓ B^{1}, A^{0} ⊔ B^{0}), ⊓_{i \in I} λ (i) : = (⊓_{i \in I} λ^{1} (i), ⨆_{i \in I} λ^{0} (i)), \\ - A : = (A^{0}, A^{1}), A - B : = A ⊓ (- B), \\ A \times C : = (A^{1} \times C^{1}, [A^{0} \times Y] ⊔ [X \times C^{0}]), \end{array}$ where $C \in E^{] [} (Y)$ . It is immediate that if $λ (0) : = A$ and $λ (1) : = B$ defines a family of complemented extensional subsets over 2, then $⨆_{i \in 2} λ (i) =_{E^{] [} (X)} A ⊔ B$ and $⊓_{i \in 2} λ (i) =_{E^{] [} (X)} A ⊓ B$ . The following diagrams depict $A ⊔ B$ , $A ⊓ B$ and $A \times C$ , respectively (the blue areas depict the 1-components and the red areas the 0-components). For the second algebra of complemented extensional subsets $B_{2}^{e} (X) : = (E^{] [} (X), \lor, \land, -)$ of X we have $\begin{array}{c} A \lor B : = ([A^{1} ⊓ B^{1}] \cup [A^{1} ⊓ B^{0}] ⊔ [A^{0} ⊓ B^{1}], A^{0} ⊓ B^{0}), \\ A \land B : = (A^{1} ⊓ B^{1}, [A^{1} ⊓ B^{0}] ⊔ [A^{0} ⊓ B^{1}] ⊔ [A^{0} ⊓ B^{0}]), \\ - A : = (A^{0}, A^{1}), A ⊟ B : = A \land (- B), \\ A ⊠ C : = (A^{1} \times C^{1}, [A^{1} \times C^{0}] ⊔ [A^{0} \times C^{1}] ⊔ [A^{0} \times C^{0}]), \\ \underset{i \in I}{⋁} λ (i) : = ([⊓_{i \in I} (λ^{1} (i) ⊔ λ^{0} (i))] ⊓ [⨆_{i \in I} λ^{1} (i)], ⊓_{i \in I} λ^{0} (i)), \\ \underset{i \in I}{⋀} λ (i) : = (⊓_{i \in I} λ^{1} (i), [⊓_{i \in I} (λ^{1} (i) ⊔ λ^{0} (i))] ⊓ [⨆_{i \in I} λ^{0} (i)]) . \end{array}$ It is straightforward to show that if $λ (0) : = A$ and $λ (1) : = B$ defines a fanily of complemented extensional subsets over 2, then $⋁_{i \in 2} λ (i) =_{E^{] [} (X)} A \lor B$ and $⋀_{i \in 2} λ (i) =_{E^{] [} (X)} A \land B$ . The following diagrams depict $A \lor B$ , $A \land B$ and $A ⊠ C$ , respectively. Notice that if $A$ , $B$ are total, complemented extensional subsets of X, then $A ⊔ B =_{E (X)} A \lor B$ and $A ⊓ B =_{E (X)} A \land B$ . In the light of Proposition 3.6, these equalities explain why Proposition 3.3 is expected to hold. Within $BRST$ , where the empty set ∅ is used, $(\emptyset, X)$ and $(X, \emptyset)$ are the bottom and top elements of $B_{1}^{e} (X)$ , respectively.24

²⁴
These definitions are also used in [14], in order to show that the second algebra of complemented subsets is a Boolean semiring with unit.

In the completely extensional framework of this section though, and following Bishop’s rejection of the empty set, we need to use the extensional empty subset

□ /_{X}

instead of ∅. Next we gather some properties of

B_{1}^{e} (X)

that are found in the definition of a swap algebra of type (I) (see Definition 7.1).

Proposition 5.1 (

INT

Let $X : = (X, =_{X}, \neq_{X})$ be a set with an extensional inequality, and if $A \in E^{] [} (X)$ , let $\begin{matrix} 0_{X} : = (□ /_{X}, X), 1_{X} : = (X, □ /_{X}), 1_{A} : = (Dom (A), □ /_{X}), 0_{A} : = (□ /_{X}, Dom (A)) . \end{matrix}$

$0_{X}$ and $1_{X}$ are the bottom and top elements of $B_{1}^{e} (X)$ , respectively.

$- 0_{X} : = 1_{X}$ and $- 0_{A} : = 1_{A}$ .

$A ⊔ (- A) =_{E^{] [} (X)} 1_{A}$ and $A ⊓ (- A) =_{E^{] [} (X)} 0_{A}$ .

$0_{X} ⊔ A =_{E^{] [} (X)} A =_{E^{] [} (X)} 0_{A} ⊔ A$ .

$0_{X} ⊓ A =_{E^{] [} (X)} 0_{X}$ and $0_{A} ⊓ A =_{E^{] [} (X)} 0_{A}$ .

$1_{X} ⊔ A =_{E^{] [} (X)} 1_{X}$ and $1_{A} ⊔ A =_{E^{] [} (X)} 1_{A}$ .

$1_{X} ⊓ A =_{E^{] [} (X)} A =_{E^{] [} (X)} 1_{A} ⊓ A$ .

$0_{- A} =_{E^{] [} (X)} 0_{A}$ .

$0_{0_{X}} =_{E^{] [} (X)} 0_{X}$ and $1_{1_{X}} =_{E^{] [} (X)} 1_{X}$ .

$0_{0_{A}} =_{E^{] [} (X)} 0_{A} =_{E^{] [} (X)} 0_{1_{A}}$ .

If X is inhabited, then $0_{X} \neq_{E^{] [} (X)} 1_{X}$ .

Proof.
Most of the equalities follow from the Ex Falso rule. For case (iii) we also use Proposition 4.9(i), and for case (v) we also use Proposition 4.7(ii). □

By Proposition 5.1(ii) $B_{1}^{e} (X)$ is not a Boolean algebra, and it is not a Heyting algebra, as if $- A = A \Rightarrow 0_{X}$ , the adjunction property for any definition of the exponential $B \Rightarrow A$ fails. In the next proof we avoid $\emptyset_{R}$ (see [3], p. 67) and we employ an $N$ -family of inhabited and coinhabited complemented subsets. Similar, but a bit more complicated, proofs can be given within all algebras of complemented subsets (categorical and extensional).
Proposition 5.2.
(i) The distributivity property $(D_{N})$ within $B_{1}^{e} (R)$ implies $LPO$ .

(ii) (INT) If $A \in E^{] [} (X)$ is total, then $(D_{I})$ within $B_{1}^{e} (X)$ holds for $A$ .
Proof.
(i) If $α : N \to 2$ , let the $N$ -family of extensional complemented subsets of $R$ $\begin{matrix} λ (n) : = \{\begin{array}{ll} ({n}^{\neq_{R}}, {n}), & α_{n} = 0 \\ ({n}, {n}^{\neq_{R}}), & α_{n} = 1 . \end{array} \end{matrix}$ If $\begin{matrix} A : = ⨆_{n \in N} - λ (n) : = (⨆_{n \in N} λ^{0} (n), ⊓_{n \in N} λ^{1} (n)), \end{matrix}$ then $\begin{array}{c} A \cup ⊓_{n \in N} λ (n) = ((⨆_{n \in N} λ^{0} (n)) \cup (⊓_{n \in N} λ^{1} (n)), (⊓_{n \in N} λ^{1} (n)) \cap (⨆_{n \in N} λ^{0} (n))), \\ ⊓_{n \in N} (A \cup λ (n)) = (⊓_{n \in N} (⨆_{n \in N} λ^{0} (n) \cup λ^{1} (n)), ⨆_{n \in N} (⊓_{n \in N} λ^{1} (n) \cap λ^{0} (n))) . \end{array}$ As $⨆_{n \in N} λ^{0} (n) \cup λ^{1} (n) \supseteq {n}^{\neq_{R}}$ , we get $⊓_{n \in N} (⨆_{n \in N} λ^{0} (n) \cup λ^{1} (n)) \supseteq N^{\neq_{R}}$ . By $(D_{N})$ we get $\begin{matrix} \frac{1}{2} \in (⨆_{n \in N} λ^{0} (n)) \cup (⊓_{n \in N} λ^{1} (n)) . \end{matrix}$ If $\frac{1}{2} \in ⨆_{n \in N} λ^{0} (n)$ , then $\frac{1}{2} \in λ^{0} (n)$ and $α_{n} = 1$ , for some n. If $\frac{1}{2} \in ⊓_{n \in N} λ^{1} (n)$ , then $α_{n} = 0$ , for every $n \in N$ .

(ii) It follows immediately by Proposition 3.2(ii). □

The final argument in the proof of Proposition 5.2(i) also shows that the hypothesis of the totality of $A$ implies $LPO$ . Next we gather some properties of $B_{2}^{e} (X)$ that are found in the definition of a swap algebra of type (II) (see Definition 7.1). Notice that there are properties that are satisfied by $B_{1}^{e} (X)$ but not by $B_{2}^{e} (X)$ , such as the absorption properties. Notice also that in contrast to $B_{1} (X)$ , $A \land B ⋢ A$ . Similarly, there are properties of $B_{2}^{e} (X)$ that are not satisfied by $B_{1}^{e} (X)$ , such as conditions (iii), (iv), (vi) and (vii) of Proposition 5.3. Notice that Proposition 5.3(viii) is the “relativised” version of the absorption equalities, which is satisfied by $B_{2}^{e} (X)$ .
Proposition 5.3 ( $INT$ ).

Let $X : = (X, =_{X}, \neq_{X})$ be a set with an extensional inequality, and let $A, B \in E^{] [} (X)$ .

$A \lor (- A) =_{E^{] [} (X)} 1_{A}$ and $A \land (- A) =_{E^{] [} (X)} 0_{A}$ .

$0_{X} \lor A =_{E^{] [} (X)} A =_{E^{] [} (X)} 0_{A} \lor A$ .

$0_{X} \land A =_{E^{] [} (X)} 0_{A} =_{E^{] [} (X)} 0_{A} \land A$ .

$1_{X} \lor A =_{E^{] [} (X)} 1_{A} =_{E^{] [} (X)} 1_{A} \lor A$ .

$1_{X} \land A =_{E^{] [} (X)} A =_{E^{] [} (X)} 1_{A} \land A$ .

$0_{A} \lor B =_{E^{] [} (X)} 1_{A} \land B$ .

$0_{A \lor B} =_{E^{] [} (X)} 0_{A \land B} =_{E^{] [} (X)} 0_{A} \lor 0_{B} =_{E^{] [} (X)} 0_{A} \land 0_{B}$ .

$(A \land B) \lor A =_{E^{] [} (X)} 1_{B} \land A =_{E^{] [} (X)} (A \lor B) \land A$ .

Proof.
Most of the equalities follow from the Ex Falso rule. For case (ii) we also use Proposition 4.7(ii) and (i). The proof of condition (vii) rests on the equalities $dom (A \lor B) =_{E (X)} dom (A \land B) =_{E (X)} dom (A) ⊓ dom (B)$ that do not hold, in general, for $A ⊔ B$ and $A ⊓ B$ . □

Next we gather the properties of $F (X, 2)$ that are also satisfied by $F^{se} (X, 2)$ . Their elaboration, in order to avoid redundancies, leads to the definition of a swap ring (Definition 8.1). Proposition 5.4.
Let the structure $(F (X, 2), +, \cdot, 0, 1, \sim, {(0_{f_{P}})}_{X_{P} \in E (X)}, {(1_{f_{P}})}_{X_{P} \in E (X)})$ , where $0$ , $1$ are the constant functions on X with values 0 and 1, respectively, and if $f_{P} : X_{P} \to 2$ , $g_{Q} : X_{Q} \to 2$ and $h_{R} : X_{R} \to 2$ , let the Boolean-valued partial functions $f_{p} + g_{Q} : X_{P} ⊓ X_{Q} \to 2$ , $f_{p} \cdot g_{Q} : X_{P} ⊓ X_{Q} \to 2$ , $g_{P \land Q} : X_{P \land Q} \to 2$ , with $g_{P \land Q} (z) : = g_{P} (z)$ . Let $\sim f_{P} : = f_{P} \circ swap$ , and $0_{f_{P}}, 1_{f_{P}} : X_{P} \to 2$ , where $0_{f_{P}} (x) : = 0$ $1_{f_{P}} (x) : = 1$ , for every $x \in X_{P}$ .

where $swap : 2 \to 2$ is defined by the rules $0 \mapsto 1$ and $1 \mapsto 0$ . Then the following equalities hold:
$(f_{P} + g_{Q}) + h_{R} =_{F (X, 2)} f_{P} + (g_{Q} + h_{R})$

$(f_{P} \cdot g_{Q}) \cdot h_{R} =_{F (X, 2)} f_{P} \cdot (g_{Q} \cdot h_{R})$

$f_{P} + g_{Q} =_{F (X, 2)} g_{Q} + f_{P}$

$f_{P} \cdot (g_{Q} + h_{R}) =_{F (X, 2)} f_{P} \cdot g_{Q} + f_{P} \cdot h_{R}$

$(g_{Q} + h_{R}) \cdot f_{P} =_{F (X, 2)} g_{Q} \cdot f_{P} + h_{R} \cdot f_{P}$

$f_{P}^{2} =_{F (X, 2)} f_{P}$

$\sim 0 =_{F (X, 2)} 1$

$\sim (\sim f_{P}) =_{F (X, 2)} f_{P}$

$f_{P} + (\sim f_{P}) =_{F (X, 2)} 1_{f_{P}}$

$f_{P} \cdot (\sim f_{P}) =_{F (X, 2)} 0_{f_{P}} =_{F (X, 2)} f_{P} + f_{P}$

$0_{f_{P}} + g_{Q} =_{F (X, 2)} g_{P \land Q} =_{F (X, 2)} 1_{f_{P}} \cdot g_{Q}$

$\sim 0_{f_{P}} =_{F (X, 2)} 1_{f_{P}}$

$0_{\sim f_{P}} =_{F (X, 2)} 0_{f_{P}}$

$0_{0} =_{F (X, 2)} 0$ and $1_{1} =_{F (X, 2)} 1$

$0_{0_{f_{P}}} =_{F (X, 2)} 0_{f_{P}} =_{F (X, 2)} 0_{1_{f_{P}}}$

$0_{f_{P} + g_{Q}} =_{F (X, 2)} 0_{f_{P} \cdot g_{Q}} =_{F (X, 2)} 0_{f_{P}} \cdot 0_{g_{Q}} =_{F (X, 2)} 0_{f_{P}} + 0_{g_{Q}} =_{F (X, 2)} 0_{f_{P}} \cdot g_{Q}$ .

$0 + f_{P} =_{F (X, 2)} f_{P} =_{F (X, 2)} 1 \cdot f_{P}$

$0 \cdot f_{P} =_{F (X, 2)} 0_{f_{P}}$ .

$\sim f_{P} =_{F (X, 2)} 1 + f_{P}$ .

If X is inhabited, then $0 \neq_{F (X, 2)} 1$ .

6. On the relation between categorical and extensional concepts related to subsets

Next we relate the proper class of the categorical subsets of a set X to the class of its extensional ones. A bounded version of Myhill’s axiom of non-choice (MANC) (or of unique choice) is crucial to this relation. According to it, $\begin{matrix} \forall_{x \in X} \exists!_{y \in Y} P (x, y) \Rightarrow \exists_{f \in F (X, Y)} \forall_{x \in X} (P (x, f (x))), \end{matrix}$ where $P (x, y)$ is an extensional property on the product $X \times Y$ of the given sets X and Y, and $\exists!_{y \in Y} P (x, y) : = \exists_{y \in Y} (P (x, y) \land \forall_{z \in Y} (P (x, z) \Rightarrow z =_{Y} y))$ . Notice that $MANC$ 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. $MANC$ , which is also considered in [1], is included in Myhill’s system $CST$ (see [26], p. 349) as a principle of generating functions. This is in contrast to Bishop’s algorithmic approach to the concept of function, hence its use in $BISH$ is questionable.

Proposition 6.1.
If $(X, =_{X})$ is a set, let the assignment routines $η : E (X) ⇝ P (X)$ and $θ : P (X) ⇝ E (X)$ , defined by $\begin{array}{c} η (X_{P}) : = (X_{P}, {id}_{P}^{X}), {id}_{P}^{X} : X_{P} ↪ X, x \mapsto x, x \in X_{P}, \\ θ (A, i_{A}^{X}) : = X_{P (A, i_{A}^{X})} : = {x \in X | \exists_{a \in A} (i_{A}^{X} (a) =_{X} x)} . \end{array}$
η and θ preserve the corresponding equalities.

$θ (η (X_{P})) =_{E (X)} X_{P}$ , for every extensional property $P (x)$ .

$η (θ (A, i_{A}^{X})) \subseteq (A, i_{A}^{X})$ , for every categorical subset $(A, i_{A}^{X})$ of X, and with the use of MANC the converse inclusion $(A, i_{A}^{X}) \subseteq η (θ (A, i_{A}^{X}))$ also holds.

(INT) If X is inhabited with an extensional inequality, then $θ (\emptyset_{X}, i_{\emptyset}^{X}) =_{E (X)} □ /_{X}$ and $η (□ /_{X}) =_{P (X)} (\emptyset_{X}, i_{\emptyset}^{X})$ .

$θ (X, {id}_{X}) =_{E (X)} X_{=_{X}}$ , $θ (A \cup B) =_{E (X)} θ (A) ⊔ θ (B)$ , and $θ (A \cap B) =_{E (X)} θ (A) ⊓ θ (B)$ .

$η (X_{=_{X}}) =_{P (X)} (X, {id}_{X})$ , $η (A ⊔ B) =_{P (X)} η (A) \cup η (B)$ , and $η (A ⊓ B) =_{P (X)} η (A) \cap η (B)$ .

Proof.
(i) Clearly, the assignment routine $i_{P}^{X}$ is an embedding, and hence η is well-defined. The bounded formula $\begin{matrix} [P (A, i_{A}^{X})] (x) : = \exists_{a \in A} (i_{A}^{X} (a) =_{X} x) \end{matrix}$ is extensional, hence θ is well-defined. It is easy to show that if $P (x)$ and $Q (x)$ are extensional properties on X, then $\begin{matrix} X_{P} =_{E (X)} X_{Q} \Leftrightarrow (X_{P}, {id}_{P}^{X}) =_{P (X)} (X_{Q}, {id}_{Q}^{X}) \Leftrightarrow X_{P} =_{V_{0}} X_{Q}, \end{matrix}$ hence η is an embedding of $E (X)$ into $P (X)$ . Let $(f, g) : (A, i_{A}^{X}) =_{P (X)} (B, i_{B}^{X})$ Then $\exists_{a \in A} (i_{A}^{X} (a) =_{X} x) \Leftrightarrow \exists_{b \in B} (i_{B}^{X} (b) =_{X} x)$ , for every $x \in X$ ; if $i_{A}^{X} (a) =_{X} x$ , for some $a \in A$ , then $i_{B}^{X} (f (a) =_{X} i_{A}^{X} (a) =_{X} x$ and if $i_{B}^{X} (b) =_{X} x$ , for some $b \in B$ , then $i_{A}^{X} (g (b) =_{X} i_{B}^{X} (b) =_{X} x$ .

(ii) By definition $θ (η (X_{P})) : = X_{P (X_{P}, id)} : = {x \in X | \exists_{y \in X_{P}} (y =_{X} x)} =_{E (X)} X_{P}$ , as if $a \in X$ such that $P (a)$ we can take $a \in X_{P}$ again with $a =_{X} a$ , while if $b \in X_{P}$ such that $b =_{X} x$ , then we get $P (x)$ by the extensionality25
²⁵
Notice that if we consider a subset $X_{S}$ of X defined by separation for a non-extensional property $S (x)$ , we cannot show a similar equality.

of P.

(iii) If $e : A ⇝ X_{P (A, i_{A}^{X})}$ is defined by the rule $a \mapsto i_{A}^{X} (a)$ , then e is a function and the following triangle commutes

We do not have a way to define explicitly an assignment routine from $X_{P (A, i_{A}^{X})}$ to A. As $i_{A}^{X}$ is an embedding, the hypothesis of $MANC$ holds for the extensional property $P (x, a) : = i_{A}^{X} (a) =_{X} x$ on $X_{P (A, i_{A}^{X})} \times A$ . By Modus Ponens we get a function $j : X_{P (A, i_{A}^{X})} \to A$ such that $i_{A}^{X} (j (x)) =_{X} x$ , for every $x \in X_{P (A, i_{A}^{X})}$ , which is the required commutativity.

(iv)–(vi) The proofs of these clauses are straightforward. □

Consequently, we need $MANC$ to show that the proper-class $P (X)$ is “equivalent” to the totality $E (X)$ . Although $E (X)$ is embedded into $P (X)$ through η, one needs $MANC$ to embed $P (X)$ into $E (X)$ . While the proper-class status of $P (X)$ should be clear, this cannot be said for $E (X)$ . What Proposition 6.1 shows is that $MANC$ should not be accepted by a constructivist26
²⁶
Myhill’s principle $MANC$ is not accepted in Sambin’s and Maietti’s “Minimalist Foundation” (see [21], p. 526).

who adheres to the set-character of $E (X)$ . A third option is to understand $E (X)$ as an impredicative set,27
²⁷
As it is remarked in [9], p. 19, “the main objection to admitting $E (X)$ into the constructive fold is that we thereby allow impredicativity, since there is then nothing to stop us considering subsets of X whose defining characteristics are self-referential”.

hence not an element of $V_{0}$ . Notice that it is also possible to define inequalities on $P (X)$ and $E (X)$ , and to show that η and θ are strongly extensional. Te assignment $η (θ)$ can be extended to set-indexed families of extensional (categorical) subsets of X, where the role of $MANC$ to the relation between these constructions is similar to its role in Proposition 6.1(iii). This role of $MANC$ in the proof of Proposition 6.1(iii) motivates the following definition.
Definition 6.2.
If $(X, =_{X})$ is a set, a categorical subset $(A, i_{A}^{X})$ of A is called a Myhill subset, if there is a function (or equivalently an embedding) $j : X_{P (A, i_{A}^{X})} \to A$ such that the following triangle commutes

We call such a function j a Myhill function.

By Proposition 6.1(ii) every categorical subset $η (X_{P})$ of X is a Myhill subset. We can find though, a set X and a categorical subset of it, which is not in the image of the corresponding class-function η. For that, it suffices to find a categorical subset $(A, i_{A}^{X})$ of X, which is Myhill but its embedding $i_{A}^{X}$ is not given by the identity rule. Let $X : = 2$ and let its categorical subset $(2, swap)$

As $\begin{matrix} 2_{P (2, swap)} : = {x \in 2 | \exists_{y \in 2} (swap (y) =_{2} x)} =_{E (2)} 2, \end{matrix}$ we take $j : = swap$ . If we avoid the use of $MANC$ , we can find a categorical subset of X that we cannot show to be Myhill, as we cannot define explicitly a Myhill function. E.g., the categorical empty set $(\emptyset_{X}, i_{\emptyset}^{X})$ of an inhabited set X in Definition 2.4 cannot shown explicitly to be a Myhill subset.
7. Swap algebras

Next we introduce swap algebras and swap algebras of type (I) and (II), as generalisations of the two algebras of complemented subsets considered in the previous sections.

Definition 7.1.
A swap algebra is a structure $A : = (A, \lor, \land, 0, 1, -, 0_{-}, 1_{-})$ , where $(A, =_{A}, \neq_{A})$ is a (class) set with an inequality, $0, 1 \in A$ , $\lor, \land, : A \times A \to A$ and $0_{-}, 1_{-} : A \to A$ are (class-)functions, such that the following conditions hold:

( ${swapa}_{1}$ ) $a \lor a =_{A} a$ .

( ${swapa}_{2}$ ) $a \lor b =_{A} b \lor a$ .

( ${swapa}_{3}$ ) $a \lor (b \lor c) =_{A} (a \lor b) \lor c$ .

( ${swapa}_{4}$ ) $a \lor (b \land c) =_{A} (a \lor b) \land (a \lor c)$ .

( ${swapa}_{5}$ ) $0 \neq_{A} 1$ .

( ${swapa}_{5}$ ) $- 0 =_{A} 1$ .

( ${swapa}_{7}$ ) $- (- a) =_{A} a$ .

( ${swapa}_{8}$ ) $- (a \lor b) =_{A} (- a) \land (- b)$ .

( ${swapa}_{9}$ ) $a \lor (- a) =_{A} 1_{a}$ and $a \land (- a) =_{A} 0_{a}$ .

( ${swapa}_{10}$ ) $a =_{A} 0_{a} \lor a$ .

A swap algebra $A$ is of type (I), if the following condition holds:

( ${swapa}_{I}$ ) $(a \lor b) \land a =_{A} a$ .

A swap algebra $A$ is of type (II), if the following condition holds:

( ${swapa}_{II}$ ) $0_{a} \lor b =_{A} 1_{a} \land b$ .

An element a of A is called total, if $1_{a} =_{A} 1$ , and it is called inhabited, if $a \neq_{A} 0_{a}$ .
Example 7.2.
By Propositions 3.2 and 5.1, if X is an inhabited set with an extensional inequality, then (within $INT$ ) $B_{1}^{e} (X)$ is a swap algebra of type (I), while by Propositions 3.5 and 5.3 $B_{2}^{e} (X)$ is a swap algebra of type (II).

If one considers formulas of a first-order theory alone, then only some of the properties of a swap algebra hold. The following proposition is straightforward to show.
Proposition 7.3 ( $MIN$ ).

Let $A_{m} (L)$ be the set of formulas of a first-order language $L$ equipped with the equality $ϕ =_{A_{m} (L)} ψ : \Leftrightarrow ⊢_{m} ϕ \Leftrightarrow ψ$ , where $⊢_{m}$ denotes derivability within minimal logic. Let $0 : = ⊥$ , $1 : = ⊤$ , $ϕ \lor ψ$ and $ϕ \land ψ$ be the disjunction and conjunction, respectively, of ϕ, ψ, $- ϕ : = \neg ϕ : = ϕ \to ⊥$ , $0_{ϕ} : = ϕ \land \neg ϕ$ and $1_{ϕ} : = ϕ \lor \neg ϕ$ . Then all conditions of a swap algebra of type (I) are satisfied, except $({swapa}_{7})$ .

Notice that within (INT) all zeros in $A_{m} (L)$ collapse to 0, and within $(CLASS)$ all ones in $A_{m} (L)$ collapse to 1. If in $A_{m} (L)$ we define $- ϕ : = ϕ^{N}$ to be the strong negation of ϕ (see [19,27,39,44]), and if $0_{ϕ} : = ϕ \land ϕ^{N}$ and $1_{ϕ} : = ϕ \lor ϕ^{N}$ , then all conditions of a swap algebra are satisfied, except $({swapa}_{7})$ , because the implication $ϕ \Rightarrow ϕ^{N N}$ , does not hold in general. In the proof of Proposition 7.3 it is the implication $\neg \neg ϕ \Rightarrow ϕ$ that does not hold, in general. If one considers though, pairs of “disjoint” formulas of a first-order theory, then one gets examples of swap algebras of both types.

Definition 7.4.
Let $A_{i} (L)$ be the set of formulas of a first-order language $L$ equipped with the equality $ϕ =_{A_{i} (L)} ψ : \Leftrightarrow ⊢_{i} ϕ \Leftrightarrow ψ$ , where $⊢_{i}$ denotes derivability within $INT$ . A(n) (intuitionistic) complemented formula is a pair $ϕ : = (ϕ^{1}, ϕ^{0})$ , where $ϕ^{1}, ϕ^{0} \in A_{i} (L)$ , such that $⊢_{i} ϕ^{1} \land ϕ^{0} \Rightarrow ⊥$ , where $⊢_{i}$ denotes intuitionistic derivability. If $ϕ : = (ϕ^{1}, ϕ^{0})$ and $ψ : = (ψ^{1}, ψ^{0})$ are complemented formulas, let $ϕ ⩽ ψ : \Leftrightarrow ⊢_{i} ϕ^{1} \Rightarrow ψ^{1} \land ψ^{0} \Rightarrow ϕ^{0}$ , and their totality $A_{i}^{⊣ ⊢} (L)$ is equipped with the equality $ϕ =_{A_{i}^{⊣ ⊢} (L)} ψ : \Leftrightarrow ϕ ⩽ ψ \land ψ ⩽ ϕ$ . Its inequality is defined by $\begin{matrix} ϕ \neq_{A_{i}^{⊣ ⊢} (L)} ψ : \Leftrightarrow \neg (ϕ^{1} \Rightarrow ψ^{1}) \lor \neg (ψ^{0} \Rightarrow ϕ^{0}) \lor \neg (ψ^{1} \Rightarrow ϕ^{1}) \lor \neg (ϕ^{0} \Rightarrow ψ^{0}) . \end{matrix}$ We call $ϕ$ total, if $ϕ^{1} \lor ϕ^{0} =_{A_{i} (L)} ⊤$ , inhabited, if $⊢_{i} ϕ^{1}$ , and coinhabited, if $⊢_{i} ϕ^{0}$ .

Clearly, if $ϕ \in A_{i} (L)$ , then $ν ϕ : = (ϕ, \neg ϕ) \in A_{i}^{⊣ ⊢} (L)$ . The inequality $(ϕ, \neg ϕ) ⩽ (ψ, \neg ψ) : \Leftrightarrow ⊢_{i} ϕ \Rightarrow ψ \land \neg ψ \Rightarrow \neg ϕ$ is reduced to $⊢_{i} ϕ \Rightarrow ψ$ . This example also shows that the definition of inequality between complemented formulas (or subsets) is a generalisation of implication and contraposition. In the case of strong negation, such that $⊢_{i} ϕ^{N} \Rightarrow \neg ϕ$ , the pair $N ϕ : = (ϕ, ϕ^{N})$ is in $A_{i}^{⊣ ⊢} (L)$ and the inequality $N ϕ ⩽ N ψ$ expresses that the Rasiowa implication (see [44]), or the strong implication (see [19]) $\begin{matrix} ϕ \overset{s}{\Rightarrow} ψ : \Leftrightarrow (ϕ \Rightarrow ψ) \land (ψ^{N} \Rightarrow ϕ^{N}) \end{matrix}$ is derivable within $INT$ . Notice that the Gödel-Gentzen translation (see e.g., [48]) preserves complemented formulas i.e., if $ϕ \in A_{i}^{⊣ ⊢} (L)$ , then $ϕ^{g} : = ({(ϕ^{1})}^{g}, {(ϕ^{0})}^{g}) \in A_{i}^{⊣ ⊢} (L)$ , as $⊢_{i} ϕ \Rightarrow ⊢_{i} ϕ^{g}$ , for every $ϕ \in A_{i} (L)$ , and $\begin{matrix} {[ϕ^{1} \land ϕ^{0} \Rightarrow ⊥]}^{g} : = {(ϕ^{1} \land ϕ^{0})}^{g} \Rightarrow ⊥^{g} : = {(ϕ^{1})}^{g} \land {(ϕ^{0})}^{g} \Rightarrow ⊥ . \end{matrix}$ The next proposition is expected and it is straightforward to show.
Proposition 7.5 (INT).

Let $0 : = (⊥, ⊤)$ and $1 : = (⊤, ⊥)$ , and if $ϕ, ψ \in A_{i}^{⊣ ⊢} (L)$ , let $\begin{matrix} 0_{ϕ} : = (⊥, ϕ^{1} \lor ϕ^{0}), 1_{ϕ} : = (ϕ^{1} \lor ϕ^{0}, ⊥), - (ϕ^{1}, ϕ^{0}) : = (ϕ^{0}, ϕ^{1}) . \end{matrix}$

(i) If we consider the operations $ϕ ⊔ ψ : = (ϕ^{1} \lor ψ^{1}, ϕ^{0} \land ψ^{0})$ and $ϕ ⊓ ψ : = (ϕ^{1} \land ψ^{1}, ϕ^{0} \lor ψ^{0})$ , then $(A_{i}^{⊣ ⊢} (L), ⊔, ⊓, 0, 1, -, 0_{-}, 1_{-})$ is a swap algebra of type (I).

(ii) If we consider the operations $\begin{array}{c} ϕ \lor ψ : = ((ϕ^{1} \land ψ^{1}) \lor (ϕ^{1} \land ψ^{0}) \lor (ϕ^{0} \land ψ^{1}), ϕ^{0} \land ψ^{0}), \\ ϕ \land ψ : = (ϕ^{1} \land ψ^{1}, (ϕ^{1} \land ψ^{0}) \lor (ϕ^{0} \land ψ^{1}) \lor (ϕ^{0} \land ψ^{0})), \end{array}$ then $(A_{i}^{⊣ ⊢} (L), \lor, \land, 0, 1, -, 0_{-}, 1_{-})$ is a swap algebra of type (II).

More examples of swap algebras can be found within the constructive measure theory of Bishop and Cheng $BCMT$ . Following [14], Theorem 4.2, the integrable sets of a complete integration space $(X, L_{1}, \int)$ i.e., the complemented subsets $A$ of X the characteristic function $χ_{A}$ of which is in $L_{1}$ and with measure $μ (A) : = \int χ_{A}$ , form a swap algebra of type (II), if the constant function 1 is in $L_{1}$ , so that $- A$ is also integrable if $A$ is integrable ( $x_{- A} = 1 + x_{A} \in L_{1}$ ). Swap algebras occur even within classical measure theory. If $X : = (X, A, μ)$ is a measure space and $A^{1}, A^{0} \in A$ , then $A^{1}$ , $A^{0}$ are μ-disjoint, if $μ (A^{1} \cap A^{0}) = 0$ . If $A$ , $B$ are pairs of μ-disjoint subsets in $A$ , then $- A, A \cup B, A \cap A, A \lor A$ and $A \land B$ are also μ-disjoint, forming a swap algebra of type (I) and (II), respectively.

Swap algebras can look quite differently from sets of pairs of appropriately disjoint objects. In [17], p. 7, a Boolean structure is associated to the set $D_{m}$ of all positive integral divisors of m, where m is a square-free natural number i.e., $m > 1$ and m has a prime decomposition of the form $m =_{N} p_{1}^{l_{1}} \cdot \dots \cdot p_{k}^{l_{k}}$ and $l_{1} =_{N} \dots =_{N} l_{k} =_{N} 1$ . It turns out that in the general case $D_{m}$ is a swap algebra of type (I).

Proposition 7.6.
If $m > 1$ , and $D_{m} : = {n \in N | n | m}$ , let $0 : = 1$ , $1 : = m$ , and let $n \lor n^{'} : = lcm {n, n^{'}}$ and $n \land n^{'} : = gcd {n, n^{'}}$ , the least common multiple and the greatest common divisor of n, $n^{'}$ , respectively. Let also $- n : = \frac{m}{n}$ , $0_{n} : = n \land (- n)$ , and $1_{n} : = n \lor (- n)$ , for every $n, n^{'} \in D_{m}$ . Then $D_{m} : = (A_{m}, \lor, \land, 0, 1, -, 0_{-}, 1_{-})$ is a swap algebra of type (I).
Proof.
If $m =_{N} p_{1}^{l_{1}} \cdot \dots \cdot p_{k}^{l_{k}}$ , and $n =_{N} p_{1}^{s_{1}} \cdot \dots \cdot p_{k}^{s_{k}} \in D_{m}$ , then $- n =_{N} p_{1}^{l_{1} - s_{1}} \cdot \dots \cdot p_{k}^{l_{k} - s_{k}} \in D_{m}$ . Then we get $\begin{array}{c} 0_{n} =_{N} p_{1}^{min {s_{1}, l_{1} - s_{1}}} \cdot \dots \cdot p_{k}^{min {s_{k}, l_{k} - s_{k}}}, \\ 1_{n} =_{N} p_{1}^{max {s_{1}, l_{1} - s_{1}}} \cdot \dots \cdot p_{k}^{max {s_{k}, l_{k} - s_{k}}} =_{D_{m}} - 0_{n} . \end{array}$ Moreover, if $k =_{N} p_{1}^{t_{1}} \cdot \dots \cdot p_{k}^{t_{k}} \in D_{m}$ , we have that $\begin{aligned} (n \lor k) \land n & =_{N} (p_{1}^{max {s_{1}, t_{1}}} \cdot \dots \cdot p_{k}^{max {s_{k}, t_{k}}}) \land (p_{1}^{s_{1}} \cdot \dots \cdot p_{k}^{s_{k}}) \\ =_{N} p_{1}^{min {max {s_{1}, t_{1}}, s_{1}}} \cdot \dots \cdot p_{k}^{min {max {s_{k}, t_{k}}, t_{k}}} \\ =_{N} p_{1}^{s_{1}} \cdot \dots \cdot p_{k}^{s_{k}} \\ =_{N} n . \end{aligned}$ All the rest properties of a swap algebra are straightforward to show. □

Clearly, $D_{p}$ is isomorphic to the Boolean algebra 2. From the previous proof we see why the swap algebra $D_{m}$ is a Boolean algebra for every square-free natural number m. If $m =_{N} p_{1}^{l_{1}} \cdot \dots \cdot p_{k}^{l_{k}}$ with $l_{1} =_{N} \dots =_{N} l_{k} =_{N} 1$ , then $\begin{matrix} n =_{N} p_{1}^{s_{1}} \cdot \dots \cdot p_{k}^{s_{k}}, - n =_{N} p_{1}^{l_{1} - s_{1}} \cdot \dots \cdot p_{k}^{l_{k} - s_{k}}, \end{matrix}$ where if $s_{i} =_{N} 0$ , then $l_{i} - s_{i} =_{N} 1$ , and if $s_{i} =_{N} 1$ , then $l_{i} - s_{i} =_{N} 0$ , therefore $min {s_{i}, l_{i} - s_{i}} =_{N} 0$ , for every $i \in {1, \dots, k}$ , and consequently $0_{n} =_{N} 0$ . Similarly, $max {s_{i}, l_{i} - s_{i}} =_{N} 1$ , for every $i \in {1, \dots, k}$ , and consequently $1_{n} =_{N} 1$ . It is also clear that $({swapa}_{II})$ does not hold in general for $D_{m}$ , as $0_{n} \lor m =_{N} m$ , while $1_{n} \land m =_{N} 1_{n}$ , which can be unequal to m. If $m =_{N} p_{1}^{l_{1}} \cdot \dots \cdot p_{k}^{l_{k}}$ , with $l_{i} > 1$ , for some $i \in {1, \dots, k}$ . then $\begin{matrix} 1_{p^{2}} =_{N} p_{i}^{2} \lor (- p_{i}^{2}) =_{N} p_{i}^{2} \lor p_{i}^{l_{i} - 2} =_{N} p_{i}^{max {2, l_{i} - 2}} . \end{matrix}$ If $m \neq_{N} p_{i}^{2}$ , then $1_{p^{2}} \neq_{N} m$ , while, if $m =_{N} p_{i}^{2}$ , then $1_{p} =_{N} p \lor p =_{N} p \neq_{N} m$ .

A swap algebra can be equivalently seen as a structure $(A, \lor, \land,^{\circ}, 0, 1)$ of type $(2, 2, 1, 0, 0)$ , such that both reducts $(A, \lor, 0)$ and $(A, \land, 1)$ are bounded semilattices (i.e. idempotent commutative monoids), ∨ distributes over ∧, and $^{\circ} : A \to A$ is an involutive map of monoids such that, for every $a \in A$ , we have that $()$ $(a \land a^{\circ}) \lor a = a$ . Note that condition $()$ , or $({swapa}_{10})$ , is an instance of absorption. Through the requirement that $^{\circ}$ is involutive and a homomorphism of monoids, both De Morgan laws hold. Moreover, ∧ distributes over ∨, whence every swap algebra is a distributive De Morgan bisemilattice (see [20]). The next two propositions are straightforward to prove.
Proposition 7.7.
If $A$ is a swap algebra, the following hold:
$a \land a =_{A} a$ .

$a \land b =_{A} b \land a$ .

$a \land (b \land c) =_{A} (a \land b) \land c$ .

$a \land (b \lor c) =_{A} (a \land b) \lor (a \land c)$ .

$- 0_{a} =_{A} 1_{a}$ .

$0_{- a} =_{A} 0_{a}$ .

$0_{0} =_{A} 0$ and $1_{1} =_{A} 1$ .

$0_{0_{a}} =_{A} 0_{a} =_{A} 0_{1_{a}}$ .

$0 \lor a =_{A} a$ .

$0_{a} \land a =_{A} 0_{a}$ .

$1 \land a =_{A} a =_{A} 1_{a} \land a$ .

$1_{a} \lor a =_{A} 1_{a}$ .

Proposition 7.8.
If $A$ is a swap algebra of type (I), the following hold:
$0 \land a =_{A} 0$ .

$1 \lor a =_{A} 1$ .

$a =_{A} (a \land b) \lor a$ .

The restriction of all operations of $A$ to its subset ${0, 1}$ is isomorphic to the Boolean algebra of 2.

As the second absorption identity (3) above is a consequence of $({swap}_{I})$ , any swap algebra of type (I) a distributive lattice. In other words, the swap algebras of type (I) are nothing but the De Morgan algebras (see [6]).
Proposition 7.9.
If $A$ is a swap algebra of type (II), the following hold:
$a \land (- a \lor b) =_{A} a \land b$ .

$a \lor (- a \land b) =_{A} a \lor b$ .

$0 \land a =_{A} 0_{a}$ .

$1 \lor a =_{A} 1_{a}$ .

$0_{a \lor b} =_{A} 0_{a \land b} =_{A} 0_{a} \lor 0_{b} =_{A} 0_{a} \land 0_{b}$ .

$0_{a} \land b =_{A} 0_{a} \land (- b) =_{A} 0_{a \land b}$ .

$(a \lor b) \land a =_{A} 1_{b} \land a =_{A} (a \land b) \lor a$ .

Proof.
(1) $a \land ((- a) \lor b) =_{A} (a \land (- a)) \lor (a \land b) =_{A} ((a \land (- a)) \lor a) \land ((a \land (- a)) \lor b) =_{A} a \land ((a \land (- a)) \lor b) =_{A} a \land ((a \lor (- a)) \land b) =_{A} (a \land (a \lor (- a))) \land b =_{A} a \land b$ .

(2) $a \lor b =_{A} - ((- a) \land (- b)) =_{A} - ((- a) \land (a \lor (- b)) =_{A} a \lor - (a \lor (- b)) =_{A} a \lor ((- a) \land b)$ .

(3) $a \land (- a) =_{A} a \land ((- a) \lor 0) =_{A} a \land 0$ .

(4) $a \lor (- a) =_{A} - ((- a) \land - (- a)) =_{A} - ((- a) \land 0) =_{A} - (- a) \lor (- 0) =_{A} a \lor 1$ .

(5) As $0_{- x} =_{A} 0_{x}$ , we have the following:

$0_{a \lor b} =_{A} (a \lor b) \land - (a \lor b) =_{A} 0 \land (a \lor b) =_{A} (0 \land a) \lor (0 \land b) =_{A} (a \land (- a)) \lor (b \land (- b)) =_{A} 0_{a} \lor 0_{b}$ .

Similarly, $0_{a \land b} =_{A} 0_{a} \land 0_{b}$ .

$0_{a \land b} =_{A} 0_{- (a \land b)} = 0_{(- a) \lor (- b)} =_{A} 0_{- a} \lor 0_{- b} =_{A} 0_{a} \lor 0_{b}$ .

Similarly, $0_{a \lor b} =_{A} 0_{a} \land 0_{b}$ .

(6) $0_{a} \land b =_{A} 0 \land a \land b =_{A} 0 \land b \land a =_{A} 0_{b} \land a =_{A} 0_{- b} \land a =_{A} 0_{a} \land (- b)$ .

Moreover, $a \land (- a) \land b =_{A} 0 \land a \land b =_{A} (a \land b) \land - (a \land b)$ .

(7) $a \land (a \lor b) =_{A} a \land ((- a) \lor (a \lor b)) =_{A} a \land ((- a) \lor ((a \land (- b)) \lor b) =_{A} a \land ((- a) \lor ((- b) \lor b)) =_{A} a \land (b \lor (- b))$ . □

In analogy to the duality principle for Boolean algebras, we have the following duality principle for swap algebras $(DPSA)$ : if an equation $(e)$ holds, then the equation $(e^{})$ also holds, where $(e^{})$ follows from $(e)$ by interchanging 0 and 1, $0_{r}$ with $1_{r}$ , ∧ and ∨. By Proposition 7.9(i) any swap algebra of type (II) is an involutive bisemilattice (see [7]). These structures have been thoroughly studied in the context of Weak Kleene Logic. Next we show that the two types of swap algebras collapse to the same structure, if the total elements of a swap algebra are considered.
Proposition 7.10.
If $A$ is a swap algebra of type (I) or (II), then its total elements $T (A)$ form a swap algebra both of type (I) and (II). Actually, $T (A)$ is a Boolean algebra. Conversely, every Boolean algebra is a swap algebra both of type (I) and (II).
Proof.
Clearly, $0, 1 \in T (A)$ , and if $a, b \in T (A)$ , then $a \lor b, a \land b \in T (A)$ . For example, we have that $\begin{aligned} 1_{a \land b} & =_{A} (a \land b) \lor - (a \land b) \\ =_{A} (a \land b) \lor [(- a) \lor (- b)] \\ =_{A} [a \lor (- a) \lor (- b)] \land [b \lor (- a) \lor (- b)] \\ =_{A} [1_{a} \lor (- b)] \land [1_{b} \lor (- a)] \\ =_{A} [1 \lor (- b)] \land [1 \lor (- a)] . \end{aligned}$ If $A$ is a swap algebra of type (I), then by Proposition 7.8(2) the right part of the last equality is equal to $1 \land 1 =_{A} 1$ , while if $A$ is a swap algebra of type (II), then by Proposition 7.9(5) it becomes $1_{- b} \land 1_{- a} =_{A} 1_{b} \land 1_{a} =_{A} 1_{a \land b} =_{A} 1_{a \lor b}$ . Clearly, if $a \in T (A)$ , then $- a \in T (A)$ . The rest is straightforward to show. □
Definition 7.11.
If $A$ , $B$ are swap algebras, an arrow $f : A \to B$ is a function $f : A \to B$ , such that $f (a \lor a^{'}) =_{B} f (a) \lor f (a^{'})$ , $f (- a) =_{B} - f (a)$ , and $f (1) =_{B} 1$ . A strong arrow $f : A \overset{s}{\to} B$ is an arrow $f : A \to B$ , such that the function $f : A \to B$ is strongly extensional. Let $SwapAlg$ be the category28
²⁸
The development of category theory within $BST$ is sketched in [32], and it is elaborated in [40].

of swap algebras and arrows, and let ${SwapAlg}^{s}$ be its subcategory of swap algebras and strong arrows. We denote by ${SwapAlg}_{I}$ and ${SwapAlg}_{I}^{s}$ the corresponding categories of swap algebras of type (I) and by ${SwapAlg}_{II}$ and ${SwapAlg}_{II}^{s}$ the corresponding categories of swap algebras of type (II).

Clearly, an arrow between swap algebras satisfies $f (0_{a}) =_{B} 0_{f (a)}$ , $f (1_{a}) =_{B} 1_{f (a)}$ , and $f (a \land a^{'}) =_{B} f (a) \land f (a^{'})$ . As an arrow between swap algebras preserves totality, the rules $A \mapsto T (A)$ and $f : A \to B \mapsto T (f) : = f_{| T (A)}$ determine a functor $T_{s a} : SwapAlg \to BooleAlg$ , or functors $T_{s a I} : {SwapAlg}_{I} \to BooleAlg$ and $T_{s a II} : {SwapAlg}_{II} \to BooleAlg$ . Clearly, we have the embedding functors $S_{a I} : BooleAlg \to {SwapAlg}_{I}$ and $S_{a II} : BooleAlg \to {SwapAlg}_{II}$ , defined by the rules $A \mapsto A$ and $f \mapsto f$ . If $B$ is a Boolean algebra, then every arrow $g : A \to B$ in ${SwapAlg}_{I}$ or in ${SwapAlg}_{I}$ determines through its restriction to $T (A)$ a homomorphism $T (A) \to B$ in $BooleAlg$ . If $f : T (A) \to B$ is a homomorphism of Boolean algebras though, we cannot extend it to an arrow $A \to B$ in ${SwapAlg}_{I}$ , or in ${SwapAlg}_{I}$ , as an object in a swap algebra is not extended appropriately to a total one. Consequently $T_{I}$ is not left-adjoint to $S_{I}$ .
8. Swap rings

Next we formulate the notion of a swap ring as an abstract version of the algebraic structure of the Boolean-valued, partial functions. Richman in [46], pp. 2682-2683, has also formulated an abstract structure motivated by the real-valued partial functions on $R$ , and especially the (explicit) algebraic functions, without developing their theory. Every swap ring is a Richman ring, in the sense of [46].

Definition 8.1.
A swap ring is a structure $R : = (R, +, \cdot, 0, 1, \sim, 0_{-}, 1_{-})$ , where $(R, =_{R}, \neq_{R})$ is a (class) set with an inequality, $0, 1 \in R$ , $+, \cdot, : R \times R \to R$ and $0_{-}, 1_{-} : R \to R$ are (class-)functions, such that the following conditions hold:

( ${swapr}_{1}$ ) $(r + s) + t =_{R} r + (s + t)$ .

( ${swapr}_{2}$ ) $(r \cdot s) \cdot t =_{R} r \cdot (s \cdot t)$ .

( ${swapr}_{3}$ ) $r + s =_{R} s + r$ .

( ${swapr}_{4}$ ) $r \cdot (s + t) =_{R} r \cdot s + r \cdot t$ .

( ${swapr}_{5}$ ) $(s + t) \cdot r =_{R} s \cdot r + t \cdot r$ .

( ${swapr}_{6}$ ) $r^{2} =_{R} r$ .

( ${swapr}_{7}$ ) $0 \neq_{R} 1$ .

( ${swapr}_{8}$ ) $\sim 0 =_{R} 1$ and $\sim 1 =_{R} 0$ .

( ${swapr}_{9}$ ) $\sim r =_{R} 1 + r$ .

( ${swapr}_{10}$ ) $r + r =_{R} 0_{r} =_{R} 0 \cdot r$ .

( ${swapr}_{11}$ ) $0_{r} + s =_{R} 1_{r} \cdot s$ .

( ${swapr}_{12}$ ) $1 \cdot r =_{R} r =_{R} r \cdot 1$ .

Totality of an element r of R, is defined as in Definition 7.1.
Example 8.2.
By Proposition 5.4 the structures associated to the sets $F (X, 2)$ and $F^{se} (X, 2)$ are swap rings.
Example 8.3.
The structure $(2, +, \cdot, 0, 1, swap, 0_{-}, 1_{-})$ , where $0_{i} : = 0$ and $1_{i} : = 1$ , for every $i \in 2$ , is a swap ring.

Next we prove some consequences of the axioms for a swap ring, such as the commutativity of multiplication.
Proposition 8.4.
If $R : = (R, +, \cdot, 0, 1, \sim, 0_{-}, 1_{-})$ is a swap ring, the following conditions hold:
$r + (\sim r) =_{R} 1_{r}$ .

$r \cdot (\sim r) =_{R} 0_{r}$ .

$\sim 0_{r} =_{R} 1_{r}$ .

$0_{1} =_{R} 0$ .

$1_{0} =_{R} 1 =_{R} 1_{1}$ .

$0 + r =_{R} r$ .

$\sim (\sim r) =_{R} r$ .

$0_{0} =_{R} 0 =_{R} 0 \cdot 0$ .

$0_{\sim r} =_{R} 0_{r}$ .

$0_{0_{r}} =_{R} 0_{r} =_{R} 0_{1_{r}}$ .

$0_{r} + 0_{s} =_{R} 0_{r \cdot s} =_{R} 0_{s \cdot r} =_{R} 0_{r} \cdot 0_{s}$ .

$0_{r} + r =_{R} r$ .

$r \cdot s =_{R} s \cdot r$ .

Proof.
(1) $r + (\sim r) =_{R} r + (1 + r) =_{R} 0_{r} + 1 =_{R} 1_{r} \cdot 1 =_{R} 1_{r}$ .

(2) $r \cdot (\sim r) =_{R} r \cdot (1 + r) =_{R} r + r^{2} =_{R} r + r =_{R} 0_{r}$ .

(3) $\sim 0_{r} =_{R} \sim (r + r) =_{R} 1 + r + r =_{R} \sim r + r =_{R} 1_{r}$ .

(4) $0_{1} =_{R} 1 + 1 =_{R} \sim 1 =_{R} 0$ .

(5) By (1) we have that $1_{0} =_{R} 0 + 1 =_{R} \sim 0 =_{R} 1$ . Moreover, $1_{1} =_{R} 1 + 0 =_{R} 0 + 1 =_{R} \sim 0 =_{R} 1$ .

(6) $0 + r =_{R} 0_{1} + r =_{R} 1_{1} \cdot r =_{R} 1 \cdot r =_{R} r$ .

(7) $\sim (\sim r) =_{R} 1 + (1 + r) =_{R} (1 + 1) + r =_{R} \sim 1 + r =_{R} 0 + r =_{R} r$ .

(8) By (6) we have that $0_{0} =_{R} 0 + 0 =_{R} 0$ . Moreover, $0 \cdot 0 =_{R} 0_{0} =_{R} 0$ .

(9) $0_{\sim r} =_{R} 0 \cdot (\sim r) =_{R} 0 \cdot (1 + r) =_{R} 0 \cdot 1 + 0 \cdot r =_{R} 0 + 0_{r} =_{R} 0_{r}$ .

(10) $0_{0_{r}} =_{R} 0 \cdot 0_{r} =_{R} 0 \cdot (0 \cdot r) =_{R} (0 \cdot 0) \cdot r =_{R} 0 \cdot r =_{R} 0_{r}$ . Moreover, by (3) and (9) we get $0_{1_{r}} =_{R} 0_{\sim 0_{r}} =_{R} 0_{0_{r}} =_{R} 0_{r}$ .

(11) $0_{r} + 0_{s} =_{R} 1_{r} \cdot 0_{s} =_{R} (r + (\sim r)) \cdot 0_{s} =_{R} r \cdot 0_{s} + (\sim r) \cdot 0_{s} =_{R} r (s + (\sim s)) + (\sim r) (s + (\sim s)) =_{R} r \cdot s + r \cdot s + (\sim r) s + (\sim r) \cdot s =_{R} 0_{r \cdot s} + 0_{(\sim r) \cdot s} =_{R} 0_{r} \cdot s + 0_{\sim r} \cdot s =_{R} 0_{r} \cdot s + 0_{r} \cdot s =_{R} 0_{0_{r \cdot s}} =_{R} 0_{r \cdot s}$ . For the second equality we work similarly.

(12) $0_{r} + r =_{R} 0 \cdot r + r =_{R} (0 + 1) \cdot r =_{R} 1 \cdot r =_{R} r$ .

(13) By (12) we have that $r \cdot s =_{R} 0 \cdot r \cdot s + r \cdot s =_{R} 0 \cdot r + 0 \cdot s + r \cdot s =_{R} 0 \cdot (r + s) + r \cdot s =_{R} ((r + s) + (r + s)) + r \cdot s =_{R} (r + s) + {(r + s)}^{2} + r \cdot s =_{R} r + s + (r + r \cdot s + s \cdot r + s) + r \cdot s =_{R} 0 \cdot r + 0 \cdot s + 0 \cdot r \cdot s + s \cdot r =_{R} 0 \cdot r \cdot s + 0 \cdot r \cdot s + s \cdot r =_{R} 0 \cdot 0 \cdot r \cdot s + s \cdot r =_{R} 0 \cdot r \cdot s + s \cdot r =_{R} 0 \cdot s \cdot r + s \cdot r =_{R} s \cdot r$ . □

By the previous proposition the subset ${0, 1}$ of a swap ring $R$ is a Boolean ring. Not only 2, but every Boolean ring (see [17]) is a swap ring in a canonical way, and the theory of swap rings is expected to be an appropriate generalisation of the theory of Boolean rings. The following proposition is straightforward to prove.
Proposition 8.5.
If $R$ is a swap ring, then its total elements $T (R)$ is a Boolean ring. Conversely, if $(R, +, \cdot, 0, 1)$ is a Boolean ring, then $R : = (R, +, \cdot, 0, 1, \sim, 0_{-}, 1_{-})$ is a swap ring, where $\sim r : = 1 + r$ , $0_{r} : = 0$ and $1_{r} : = 1$ , for every $r \in R$ .

An alternative formulation of a swap ring can also be given, similar to the previously mentioned alternative definition of a swap algebra, where by definition we have that $0_{r} : = 0 \cdot r$ and $1_{r} : = 0_{r}^{'}$ , for every $r \in R$ . According to it, a swap ring is a multiplicatively idempotent semiring $(R, +, \cdot, 0, 1)$ with involution ′ such that, for every $r, s \in S$ , we have that $0^{'} =_{R} 1$ , $r^{'} =_{R} 1 + r$ , $0 \cdot r + s =_{R} {(0 \cdot r)}^{'} s$ , and $0 \cdot r =_{R} r + r$ . Here a more general understanding of semirings is used, in that we do not demand that $0$ be absorbing, something which is also considered in [47]. A swap ring generates a swap algebra exactly in the same way a Boolean ring generates a Boolean algebra. Actually, a swap ring generates in a canonical way a swap algebra of type (II), a fact which reflects the compatibility of the second algebra of complemented subsets with the boolean-valued partial functions in Proposition 3.6. The converse is also the case, as for Boolean algebras and Boolean rings
Proposition 8.6.
If $R : = (R, +, \cdot, 0, 1, \sim, 0_{-}, 1_{-})$ is a swap ring, then $A_{s} (R) : = (R, \lor, \land, 0, 1, -, 0_{-}, 1_{-})$ is a swap algebra of type (II), where $r \lor s : = r + s + r \cdot s$ , $r \land s : = r \cdot s$ and $- r : = 1 + r$ , for every $r, s \in R$ . Conversely, if $A : = (A, \lor, \land, 0, 1, -, 0_{-}, 1_{-})$ is a swap algebra of type (II), then $R_{s} (A) : = (A, + . \cdot, 0, 1, \sim, 0_{-}, 1_{-})$ is a swap ring, where $\sim a : = - a$ , $a \cdot b : = a \land b$ , and $a + b : = (a \land (- b)) \lor ((- a) \land b)$ , for every $a, b \in A$ . Moreover, the two constructions are inverse to each other.
Proof.
We show only that $R_{s} (A)$ is a swap ring, using Proposition 7.9. We have that $\begin{matrix} 1 + a =_{A} [1 \land (- a)] \lor [(- 1) \land a] =_{A} - a \lor 0_{a} =_{A} - a \lor 0_{- a} =_{A} - a = : \sim a . \end{matrix}$ Note that $\begin{array}{c} a + 0 =_{A} (a \land (- 0)) \lor ((- a) \land 0) =_{A} (a \land 1) \lor ((- a) \land 0) =_{A} a \lor {((- a) \land 0)}_{A} = a \lor 0 =_{A} a \\ (a \land (- b)) \lor ((- a) \land b) =_{A} ((a \land (- b)) \lor (- a)) \land ((a \land (- b)) \lor b) =_{A} ((- a) \lor (- b)) \land (a \lor b) . \end{array}$ Thus, in order to see that + is associative, we may follow the symbolic proof of the associativity of symmetric difference, whence $(A, +, 0)$ is a commutative monoid. Next, to see that · distributes over +, observe that $\begin{aligned} a \cdot b + a \cdot c & =_{A} ((a \land b) \land - (a \land c)) \lor (- (a \land b) \land (a \land c)) \\ =_{A} (a \land b \land (- a \lor (- c)) \lor ((- a) \lor (- b)) \land a \land c) \\ =_{A} (a \land ((- a) \lor (- c)) \land b) \lor (a \land ((- a) \lor (- b)) \land c) \\ =_{A} (a \land (- c) \land b) \lor (a \land (- b) \land c) (by Proposition 7.9(6)) \\ =_{A} (a \land b \land (- c)) \lor (a \land (- b) \land c) \\ =_{A} a \land ((b \land (- c)) \lor ((- b) \land c)) \\ =_{A} a \cdot (b + c) . \end{aligned}$ Moreover, $a + a =_{A} (a \land (- a)) \lor ((- a) \land a) =_{A} a \land (- a)$ . Finally, we show condition $({swapr}_{11})$ as follows: $\begin{aligned} 0_{a} + b & =_{A} ((0 \land a) \land (- b)) \lor (- (0 \land a) \land b) \\ =_{A} ((a \land (- a)) \land (- b)) \lor (- (a \land (- a)) \land b) \\ =_{A} ((a \land (- a)) \land (- b)) \lor ((a \lor (- a)) \land b) \\ =_{A} ((a \land (- a)) \land (- b)) \lor ((a \land (- a)) \lor b) \\ =_{A} b \lor ((- b) \land (a \land (- a))) \lor (a \land (- a)) \\ =_{A} b \lor (a \land (- a)) \lor (a \land (- a)) \\ =_{A} b \lor (a \land (- a)) \\ =_{A} (a \lor (- a)) \land b \\ =_{A} - (a \land (- a)) \land b \\ =_{A} - (0 \land a) \land b \\ =_{A} 1_{a} \cdot b . \end{aligned}$ We skip the cumbersome calculations that show that the above constructions are inverse to each other. Notice though, that the axiom $({swapr}_{9})$ is crucial to the proof that these constructions are inverse to each other. □
Definition 8.7.
If $R$ , $S$ are swap rings, an arrow $f : R \to S$ is a function $f : R \to S$ , such that $f (r + r^{'}) =_{S} f (r) + f (r^{'})$ , $f (r \cdot r^{'}) =_{S} f (r) \cdot f (r^{'})$ , and $f (1) =_{S} 1$ . A strong arrow $f : R \overset{s}{\to} S$ is an arrow $f : R \to S$ , such that the function $f : A \to B$ is strongly extensional. Let $SwapRing$ be the category of swap rings and arrows, and let ${SwapRing}^{s}$ be its subcategory of swap rings and strong arrows.

An arrow f as above satisfies $f (- r) =_{S} - f (r)$ , $f (0_{r}) =_{S} 0_{f (r)}$ , $f (1_{r}) =_{S} 1_{f (r)}$ , and hence f preserves totality. The following proposition is straightforward to show. Proposition 8.8.
Let $T_{s r} : SwapRing \to BooleRing$ be the functor defined by the rules $R \mapsto T (R)$ and $f \mapsto f_{| T (R)}$ , and let $A_{s} : SwapRing \to {SwapAlg}_{II}$ be the functor defined by the rules $R \mapsto A_{s} (R)$ and $f \mapsto f$ .

(i) If $R$ is a swap ring and $r \in R$ , then r is total in $R$ if and only if r is total in the swap algebra of type (II) $A_{s} (R)$ .

(ii) If $A_{b} : BooleRing \to BooleAlg$ is the standard functor associating a Boolean algebra to a Boolean ring, then the following rectangle commutes

9. Conclusions and future work

Mathematics becomes computationally more informative, if, instead of classical logic, intuitionistic logic is used. Pioneers, such as Brouwer, realised early on that negation does not suit well to constructive reasoning and replaced negatively defined concepts by positive ones. Intuitionists, such as Griss [16], even suggested to avoid negation completely in mathematics. Bishop, motivated by Brouwer’s inequalities, defined, the so-called here, $f$ -inequalities in a fully positive manner. Moreover, by extending the idea of positive separation from points to subsets, Bishop introduced the notion of complemented subset. As we saw, the complement $- A$ of $A$ behaves a lot like the classical complement $X ∖ A$ , where $A \subseteq X$ . Moreover, a characteristic function $χ_{A}$ is defined through $A$ . However, $χ_{A}$ is partial. The correspondence between complemented subsets and strongly extensional, Boolean-valued, partial functions, described here in Propositions 2.14 and 3.6, is behind the successful reconstruction of the Daniell approach to measure theory within Bishop-style constructive mathematics $BISH$ . Moreover, the fruitfulness of Bishop-Cheng measure theory turned complemented subsets and partial functions into “first-class citizens” in $BISH$ .

Here we presented the basic properties of the two algebras of complemented subsets, both within the categorical and the extensional powerset. The two frameworks are connected through Myhill’s axiom $MANC$ , which can be bypassed, if the non-controversial Myhill subsets are used instead. The study of the class of Myhill subsets seems to us an interesting new topic. The abstract formulation of Bishop’s algebras led us to the notions of swap algebras of type (I) and (II), while the abstract formulation of the properties of Boolean-valued partial functions led us to the notion of swap ring. These structures are interesting both from the constructive and the classical point of view, as every Boolean algebra is a swap algebra and every Boolean ring is a swap ring. Moreover, there are examples of swap algebras, like the one in Proposition 7.6, that are of interest to a classical mathematician too. More connections between swap algebras and other structures within abstract lattice theory are possible. Bishop’s first algebra of complemented subsets is an instance of a widely used construction of Kleene lattices, commonly ascribed to Kalman [18]. Using intuitionistic logic, this is to say that $B_{1} (X)$ is a distributive lattice with contravariant involution − such that $A \cap - A \subseteq B \cup - B$ , for every inhabited (or coinhabited) $A, B \in P^{) (} (X)$ . As opposed to $B_{1} (X)$ , Bishop’s second algebra $B_{2} (X)$ is not a lattice. If I is a given set, the study of the following I-distributive law $\begin{matrix} 1_{a} \land (a \lor \underset{i \in I}{⋀} a_{i}) =_{A} 1_{a} \land [\underset{i \in I}{⋀} (a \lor a_{i})] \end{matrix}$ in the context of swap algebras is an important topic, connected to the generalisation of the notion of a complete Boolean algebra. It might be interesting to relate swap algebras to overlap algebras [11,12]. While the latter provide a constructive view of complete Boolean algebras, and thus of powerset lattices, the former should serve towards an analogous and point-free treatment of algebras of complemented subsets.

In this paper the role of inequality on a the carrier set of a swap algebra and a swap ring is limited to axioms $({swapa}_{5})$ and $({swapr}_{7})$ , respectively. We could add more axioms concerning the compatibility of the operations of a swap algebra (ring) with the given inequality of its carrier set, as in the case of a Boolean ring with a strong apartness relation in [14]. Similarly to [14], the study of measures on Boolean rings with a strong apartness relation is expected to be extended to the study of measures on swap algebras with a strong inequality. Various aspects of the theory of Boolean algebras are expected to have their counterpart to the theory of swap algebras, such as the theory of ideals of Boolean algebras, and the Stone representation theorem. The study of a Stone-type representation of swap algebras, maybe in a fashion similar to [20], is an important enterprise within the theory of swap algebras. The study of the categories of swap algebras and swap rings introduced here29

²⁹

The relation of complemented subsets to Chu categories was noticed by Shulman [49], and it is also studied in [35].

is one further direction of research.

References

M.J.

Beeson, Formalizing constructive mathematics: Why and how, in: Constructive Mathematics, LNM, Vol. 873, Springer-Verlag, 1981, pp. 146–190.

M.J.

Beeson, Foundations of Constructive Mathematics, Ergebnisse der Mathematik und ihrer Grenzgebiete, Springer Verlag, 1985.

Bishop, Foundations of Constructive Analysis, McGraw-Hill, 1967.

Bishop and

D.S.

Bridges, Constructive Analysis, Grundlehren der math. Wissenschaften, Vol. 279, Springer-Verlag, Heidelberg-Berlin-New York, 1985.

Bishop and

Cheng, Constructive Measure Theory, Mem. Amer. Math. Soc., Vol. 116, 1972.

T.S.

Blyth and

J.C.

Varlet, Ockham Algebras, Oxford University Press, 1994.

Bonzio,

Gil-Férez,

Paoli and

Peruzzi, On paraconsistent weak Kleene logic: Axiomatisation and algebraic analysis, Studia Logica105(2) (2017), 253–297. doi:10.1007/s11225-016-9689-5.

D.S.

Bridges and

Richman, Varieties of Constructive Mathematics, Cambridge University Press, 1987.

D.S.

Bridges and

L.S.

Vîţă, Techniques of Constructive Analysis, Universitext, Springer, New York, 2006.

10.

D.S.

Bridges and

L.S.

Vîţă, Apartness and Uniformity: A Constructive Development, CiE Series “Theory and Applications of Computability”, Springer Verlag, Berlin Heidelberg, 2011.

11.

Ciraulo and

Contente, Overlap algebras: A constructive look at complete Boolean algebras, Log. Methods Comput. Sci.16(1) (2020), 13:1–13:15.

12.

Ciraulo and

Sambin, The overlap algebra of regular opens, J. Pure Appl. Algebra214(11) (2010), 1988–1995. doi:10.1016/j.jpaa.2010.02.002.

13.

Coquand, Universe of Bishop sets, 2017, manuscript.

14.

Coquand and

Palmgren, Metric Boolean algebras and constructive measure theory, Arch. Math. Logic41 (2002), 687–704. doi:10.1007/s001530100123.

15.

Diener, Constructive reverse mathematics (2020). arXiv:1804.05495.

16.

G.F.

Griss, Negationless intuitionistic mathematics I, Indagationes Mathematicae8 (1946), 675–681.

17.

P.R.

Halmos, Lectures on Boolean Algebras, Springer-Verlag, 1974.

18.

J.A.

Kalman, Lattices with involution, Trans. Amer. Math. Soc.87 (1958), 485–491. doi:10.1090/S0002-9947-1958-0095135-X.

19.

Köpp and

Petrakis, Strong negation in the theory of computable functionals TCF, 2023, available at: https://arxiv.org/abs/2210.05491.

20.

Ledda, Stone-type representations and dualities for varieties of bisemilattices, Studia Logica106(2) (2018), 417–448. doi:10.1007/s11225-017-9745-9.

21.

M.E.

Maietti and

Sambin, The minimalist foundation and Bishop’s constructive mathematics, in: Handbook of Constructive Mathematics,

D.S.

Bridgeset al., eds, Cambridge University Press, 2023, pp. 525–563.

22.

Martin-Löf, An intuitionistic theory of types: Predicative part, in: Logic Colloquium’73, Proceedings of the Logic Colloquium,

H.E.

Rose and

J.C.

Shepherdson, eds, Studies in Logic and the Foundations of Mathematics, Vol. 80, North-Holland, 1975, pp. 73–118. doi:10.1016/S0049-237X(08)71945-1.

23.

Martin-Löf, Intuitionistic Type Theory: Notes by Giovanni Sambin on a Series of Lectures Given in Padua, June 1980, Bibliopolis, Napoli, 1984.

24.

Martin-Löf, An intuitionistic theory of types, in: Twenty-Five Years of Constructive Type Theory, Venice, 1995,

Sambin and

J.M.

Smith, eds, Oxford Logic Guides, Vol. 36, Oxford University Press, 1998, pp. 127–172.

25.

Mines,

Richman and

Ruitenburg, A Course in Constructive Algebra, Springer Science + Business Media, New York, 1988.

26.

Myhill, Constructive set theory, The Journal of Symbolic Logic40 (1975), 347–382. doi:10.2307/2272159.

27.

Nelson, Constructible falsity, The Journal of Symbolic Logic14(1) (1949), 16–26. doi:10.2307/2268973.

28.

Palmgren, Constructivist and structuralist foundations: Bishop’s and Lawvere’s theories of sets, Annals of Pure and Applied Logic163 (2012), 1384–1399. doi:10.1016/j.apal.2012.01.011.

29.

Palmgren, Constructions of categories of setoids from proof-irrelevant families, Archive for Mathematical Logic56 (2017), 51–66. doi:10.1007/s00153-016-0514-7.

30.

Palmgren and

Wilander, Constructing categories and setoids of setoids in type theory, Logical Methods in Computer Science10(3), (2014), paper 25.

31.

Petrakis, Constructive topology of Bishop spaces, PhD thesis, LMU, Munich, 2015.

32.

Petrakis, in: Families of sets in Bishop set theory, Habilitationsschrift, LMU, Munich, 2020, available at: https://www.mathematik.uni-muenchen.de/~petrakis/.

33.

Petrakis, Embeddings of Bishop spaces, Journal of Logic and Computation30(1) (2020), 349–379. doi:10.1093/logcom/exaa015.

34.

Petrakis, Direct spectra of Bishop spaces and their limits, Logical Methods in Computer Science17(2) (2021), 4:1–4:50.

35.

Petrakis, Chu representations of categories related to constructive mathematics, 2021. arXiv:2106.01878v1.

36.

Petrakis, Proof-relevance in Bishop-style constructive mathematics, Mathematical Structures in Computer Science32(1) (2022), 1–43. doi:10.1017/S0960129522000159.

37.

Petrakis, Closed subsets in Bishop topological groups, Theoretical Computer Science935 (2022), 128–143. doi:10.1016/j.tcs.2022.09.004.

38.

Petrakis, Sets completely separated by functions in Bishop set theory, 2022, submitted.

39.

Petrakis, Strong negation in constructive mathematics, 2024, in preparation.

40.

Petrakis, Categories within Bishop set theory, 2024, in preparation.

41.

Petrakis, Bases of pseudocompact Bishop spaces, in: Handbook of Constructive Mathematics,

D.S.

Bridgeset al., eds, Cambridge University Press, 2023, pp. 359–394.

42.

Petrakis and

Wessel, Algebras of complemented subsets, in: Revolutions and Revelations in Computability,

Bergeret al., eds, Lecture Notes in Computer Science, Vol. 13359, CiE, 2022, pp. 246–258, Springer, 2022. doi:10.1007/978-3-031-08740-0_21.

43.

Petrakis and

Zeuner, Pre-measure spaces and pre-integration spaces in predicative Bishop-Cheng measure theory, 2022, submitted.

44.

Rasiowa, An Algebraic Approach to Non-classical Logics, North-Holland, 1974.

45.

Richman, Constructive Mathematics, LNM, Vol. 873, Springer-Verlag, 1981.

46.

Richman, Algebraic functions, calculus style, Communications in Algebra40 (2012), 2671–2683. doi:10.1080/00927872.2011.584337.

47.

A.B.

Romanowska and

J.D.H.

Smith, Modes, World Scientific, 2002.

48.

Schwichtenberg and

Wainer, Proofs and Computations, Perspectives in Logic, Association for Symbolic Logic and, Cambridge University Press, 2012.

49.

Shulman, Affine logic for constructive mathematics, The Bulletin of Symbolic Logic28(3) (2022), 327–386. doi:10.1017/bsl.2022.28.

50.

The Univalent Foundations Program, Homotopy Type Theory Univalent Foundations of Mathematics, Institute for Advanced Study, Princeton, 2013.

Complemented subsets and Boolean-valued,partial functions

Abstract

Keywords

1. Introduction

10 The totality A ∩ B in Definition 2.5 is defined by separation on A × B but its equality is not inherited from = A × B .

Definition 2.4 (Categorical empty subset).

Definition 3.1 (The first algebra).

Definition 4.1 (Extensional subsets).

18 Notice that in MLTT a property on a type X is described as a type family P : X → U over X, where U is a universe and X : U , and it is always extensional through the corresponding transport-term (see [50], Section 2.3).

24 These definitions are also used in [14], in order to show that the second algebra of complemented subsets is a Boolean semiring with unit.

References

¹⁰
The totality $A \cap B$ in Definition 2.5 is defined by separation on $A \times B$ but its equality is not inherited from $=_{A \times B}$ .

¹⁸
Notice that in $MLTT$ a property on a type X is described as a type family $P : X \to U$ over X, where $U$ is a universe and $X : U$ , and it is always extensional through the corresponding transport-term (see [50], Section 2.3).

²⁴
These definitions are also used in [14], in order to show that the second algebra of complemented subsets is a Boolean semiring with unit.