(i) First we show that $\gamma_{ij}$ is well-defined i.e., $\big[\gamma_{ij}(\Psi^i)\big]^j \in \Map(K^j,
\Lambda^j)$. If $n, n{'} \in \mu_0 (j)$, we show that the following diagram commutes

(E) at (0,0) $\lambda_0^j(n)$;
[right=of E] (L) ;
[right=of L] (F) $\lambda_0^j(n{'})$.;
[above=of F] (A) $\kappa_0^j(n{'})$;
[above=of E] (D) $\kappa_0^j(n)$;

[->] (E)–(F) node [midway,below]$\lambda^j_{nn{'}}$;
[->] (D)–(A) node [midway,above] $\kappa^j_{nn{'}}$;
[->] (D)–(E) node [midway,left] $\big[\gamma_{ij}(\Psi^i)\big]_n^j$;
[->] (A)–(F) node [midway,right] $\big[\gamma_{ij}(\Psi^i)\big]_{n{'}}^j$;

By definition we have that
$ \big[\gamma_{ij}(\Psi^i)\big]_{n{'}}^j \circ \kappa^j_{nn{'}} := \big[\lambda^{ij}_{\mu_{ji}(n{'})n{'}} \circ
\Psi^i_{\mu_{ji}(n{'})} \circ \kappa^{ji}_{n{'} \mu_{ji}(n{'})}\big] \circ \kappa^j_{nn{'}}$.
Since $\Psi^i$ is in $\Map(K_i^{0,M}, \Lambda_i^{0,M})$, by the commutativity of the following diagram

(E) at (0,0) $\lambda_0^i(\mu_{ji}(n))$;
[right=of E] (L) ;
[right=of L] (F) $\lambda_0^i(\mu_{ji}(n{'}))$,;
[above=of F] (A) $\kappa_0^i(\mu_{ji}(n{'}))$;
[above=of E] (D) $\kappa_0^i(\mu_{ji}(n))$;

[->] (E)–(F) node [midway,below]$\lambda^i_{\mu_{ji}(n)\mu_{ji}(n{'})}$;
[->] (D)–(A) node [midway,above] $\kappa^i_{\mu_{ji}(n)\mu_{ji}(n{'})}$;
[->] (D)–(E) node [midway,left] $\Psi^i_{\mu_{ji}(n)}$;
[->] (A)–(F) node [midway,right] $\Psi^i_{\mu_{ji}(n{'})}$;

we get $\Psi^i_{\mu_{ji}(n{'})} \circ \kappa^i_{\mu_{ji}(n)\mu_{ji}(n{'})} =
\lambda^i_{\mu_{ji}(n)\mu_{ji}(n{'})} \circ \Psi^i_{\mu_{ji}(n)}$, and hence

\begin{align*}
\Psi^i_{\mu_{ji}(n{'})} \circ \kappa^{ji}_{n{'} \mu_{ji}(n{'})} & = \Psi^i_{\mu_{ji}(n{'})}
\circ \big(\kappa^i_{\mu_{ji}(n)\mu_{ji}(n{'})} \circ \kappa^{ji}_{n{'}\mu_{ji}(n)}\big)\\
& := \big(\Psi^i_{\mu_{ji}(n{'})} \circ \kappa^i_{\mu_{ji}(n)\mu_{ji}(n{'})}\big) \circ \kappa^{ji}_{n{'}\mu_{ji}(n)}\\
& = \big(\lambda^i_{\mu_{ji}(n)\mu_{ji}(n{'})} \circ \Psi^i_{\mu_{ji}(n)}\big) \circ \kappa^{ji}_{n{'}\mu_{ji}(n)},
\end{align*}

\begin{align*}
\big[\gamma_{ij}(\Psi^i)\big]_{n{'}}  \circ \kappa^j_{nn{'}} & := \big[\lambda^{ij}_{\mu_{ji}(n{'})n{'}}
\circ \big(\Psi^i_{\mu_{ji}(n{'})} \circ \kappa^{ji}_{n{'} \mu_{ji}(n{'})}\big)\big] \circ \kappa^j_{nn{'}}\\
& = \big[\lambda^{ij}_{\mu_{ji}(n{'})n{'}} \circ \big(\big(\lambda^i_{\mu_{ji}(n)\mu_{ji}(n{'})} \circ
\Psi^i_{\mu_{ji}(n)}\big) \circ \kappa^{ji}_{n{'}\mu_{ji}(n)}\big)\big] \circ \kappa^j_{nn{'}}\\
& := \big(\lambda^{ij}_{\mu_{ji}(n{'})n{'}} \circ \lambda^i_{\mu_{ji}(n)\mu_{ji}(n{'})}\big) \circ
\Psi^i_{\mu_{ji}(n)} \circ \big(\kappa^{ji}_{n{'}\mu_{ji}(n)} \circ \kappa^j_{nn{'}}\big)\\
& = \lambda^{ij}_{\mu_{ji}(n)n{'}} \circ \Psi^i_{\mu_{ji}(n)}  \circ \kappa^{ji}_{n\mu_{ji}(n)}\\
& = \lambda^j_{nn{'}} \circ \big(\lambda^{ij}_{\mu_{ji}(n)n} \circ \Psi^i_{\mu_{ji}(n)}  \circ
\kappa^{ji}_{n\mu_{ji}(n)}\big)\\
& := \lambda^j_{nn{'}} \circ \big[\gamma_{ij}(\Psi^i)\big]_{n}^j.
\end{align*}

If $\Psi^i = \Phi^i$, we show that $\big[\gamma_{ij}(\Psi^i)\big]^j = \big[\gamma_{ij}(\Phi^i)\big]^j$.

\[ [\gamma_{ij}(\Psi^i)]_n^j :=  \lambda^{ij}_{\mu_{ji}(n)n} \circ \Psi^i_{\mu_{ji}(n)}  \circ
\kappa^{ji}_{n \mu_{ji}(n)} \ \ \ \& \ \ \
[\gamma_{ij}(\Phi^i)]_n^j := \lambda^{ij}_{\mu_{ji}(n)n} \circ \Phi^i_{\mu_{ji}(n)} \circ \kappa^{ji}_{n \mu_{ji}(n)}, \]

and since $\Psi^i = \Phi^i$, we get $\Psi^i_{\mu_{ji}(n)} = \Phi^i_{\mu_{ji}(n)}$, and hence the
following diagram commutes

(E) at (0,0) $\kappa_0^j(n)$;
[right=of E] (K) ;
[right=of K] (L) ;
[right=of L] (M) ;
[right=of M] (F) $\lambda_0^j(n)$.;
[above=of F] (A) $\lambda_0^j(n)$;
[above=of E] (D) $\kappa_0^j(n)$;

[->] (E)–(F) node [midway,below]$\lambda^{ij}_{\mu_{ji}(n)n} \circ \Phi^i_{\mu_{ji}(n)}
\circ \kappa^{ji}_{n \mu_{ji}(n)}$;
[->] (D)–(A) node [midway,above] $\lambda^{ij}_{\mu_{ji}(n)n} \circ \Psi^i_{\mu_{ji}(n)}
\circ \kappa^{ji}_{n \mu_{ji}(n)}$;
[->] (D)–(E) node [midway,left] $\kappa^j_{nn}$;
[->] (A)–(F) node [midway,right] $\lambda^j_{nn}$;

(ii) If $m \in \mu_0 (i)$, then $[\gamma_{ii}(\Psi^i)]_m^i := \lambda^{ii}_{\mu_{ii}(m)m} \circ
\Psi^i_{\mu_{ii}(m)}  \circ \kappa^{ii}_{m \mu_{ii}(m)} := \lambda^{ii}_{mm} \circ \Psi^i_{m}
\circ \kappa^{ii}_{mm}
:= \id_{\lambda_0^i (m)}  \circ \Psi^i_{m}  \circ \id_{\kappa_0^i (m)}
:= \Psi^i_{m},$
hence $[\gamma_{ii}(\Psi^i)]_m^i := \Psi^i_m$, and consequently $\big[\gamma_{ii}(\Psi^i)\big]^i
:= \Psi^i$. For the commutativity of the diagram

(E) at (0,0) $\Map\big(K_j^{0,M}, \Lambda_j^{0,M}\big)$;
[right=of E] (L) ;
[right=of L] (F) $\Map\big(K_k^{0,M}, \Lambda_k^{0,M}\big)$;
[above=of E] (D) $\Map\big(K_i^{0,M}, \Lambda_i^{0,M}\big)$;

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

we need to show the equality between the  maps

\[ \chi^k_l := \lambda^{jk}_{\mu_{kj}(l)l} \circ \big[\gamma_{ij}(\Psi^i)\big]^j_{\mu_{kj}(l)}
\circ \kappa^{kj}_{l \mu_{kj}(l)} \ \ \ \& \ \ \
\upsilon^k_l := \lambda^{ik}_{\mu_{ki}(l)l} \circ \Psi^j_{\mu_{ki}(l)}  \circ \kappa^{ki}_{l \mu_{ki}(l)}. \]

By the definition of $\big[\gamma_{ij}(\Psi^i)\big]^j_{\mu_{kj}(l)}$ we get

\begin{align*}
\chi^k_l & := \lambda^{jk}_{\mu_{kj}(l)l} \circ \big(\lambda^{ij}_{\mu_{ji}(\mu_{kj}(l))\mu_{kj}(l)}
\circ \Psi^i_{\mu_{ji}(\mu_{kj}(l))}  \circ \kappa^{ji}_{\mu_{kj}(l) \mu_{ji}(\mu_{kj}(l))}\big)
\circ \kappa^{kj}_{l \mu_{kj}(l)}\\
& = \big(\lambda^{jk}_{\mu_{kj}(l)l} \circ \lambda^{ij}_{\mu_{ji}(\mu_{kj}(l))\mu_{kj}(l)}\big)
\circ \Psi^i_{\mu_{ji}(\mu_{kj}(l))}  \circ \big(\kappa^{ji}_{\mu_{kj}(l) \mu_{ji}(\mu_{kj}(l))}
\circ \kappa^{kj}_{l \mu_{kj}(l)}\big)\\
& = \lambda^{ik}_{\mu_{ji}(\mu_{kj}(l))l} \circ \Psi^i_{\mu_{ji}(\mu_{kj}(l))}  \circ
\kappa^{ki}_{l \mu_{ji}(\mu_{kj}(l))}.
\end{align*}

By the supposed commutativity of the following diagram

(E) at (0,0) $\lambda_0^i (\mu_{ki}(l))$;
[right=of E] (K) ;
[right=of K] (L) ;
[right=of L] (F) $\lambda_0^i (\mu_{ji}(\mu_{kj}(l)))$,;
[above=of F] (A) $\kappa_0^i(\mu_{ji}(\mu_{kj}(l)))$;
[above=of E] (D) $\kappa_0^i(\mu_{ki}(l))$;

[->] (E)–(F) node [midway,below]$\lambda^i_{\mu_{ki}(l)\mu_{ji}(\mu_{kj}(l))}$;
[->] (D)–(A) node [midway,above] $\kappa^i_{\mu_{ki}(l)\mu_{ji}(\mu_{kj}(l))}$;
[->] (D)–(E) node [midway,left] $\Psi^i_{\mu_{ki}(l)}$;
[->] (A)–(F) node [midway,right] $\Psi^i_{\mu_{ji}(\mu_{kj}(l))}$;

\begin{align*}
\upsilon^k_l & := \lambda^{ik}_{\mu_{ki}(l)l} \circ \Psi^j_{\mu_{ki}(l)}  \circ
\kappa^{ki}_{l \mu_{ki}(l)}\\
& = \lambda^{ik}_{\mu_{ji}(\mu_{kj}(l))l} \circ \big(\lambda^{i}_{\mu_{ki}(l)\mu_{ji}(\mu_{kj}(l))}
\circ \Psi^j_{\mu_{ki}(l)} \big) \circ \kappa^{ki}_{l \mu_{ki}(l)}\\
& = \lambda^{ik}_{\mu_{ji}(\mu_{kj}(l))l} \circ \big(\Psi^i_{\mu_{ji}(\mu_{kj}(l))}
\circ \kappa^i_{\mu_{ki}(l)\mu_{ji}(\mu_{kj}(l))} \big) \circ \kappa^{ki}_{l \mu_{ki}(l)}\\
& = \lambda^{ik}_{\mu_{ji}(\mu_{kj}(l))l} \circ \Psi^i_{\mu_{ji}(\mu_{kj}(l))} \circ
\big(\kappa^i_{\mu_{ki}(l)\mu_{ji}(\mu_{kj}(l))} \circ \kappa^{ki}_{l \mu_{ki}(l)}\big)\\
& = \lambda^{ik}_{\mu_{ji}(\mu_{kj}(l))l} \circ \Psi^i_{\mu_{ji}(\mu_{kj}(l))} \circ
\kappa^{ki}_{l \mu_{ji}(\mu_{kj}(l))}\\
& = \chi^k_l.\qedhere
\end{align*}

If $(K^i)_{i \in I}, (\Lambda^i)_{i \in I}  \in \Fam(I, M)$, a family of families-map
from $(K^i)_{i \in I}$ to $(\Lambda^i)_{i \in I}$family of families-map, in symbols
$\Psi \colon (K^i)_{i \in I} \To (\Lambda^i)_{i \in I}$,
is a dependent operation
$\Psi \colon \bigcurlywedge_{i \in I}\Map\big(K_i^{0,M}, \Lambda_i^{0,M}\big)$

such that for every $(i, j) \in D(I)$ the following diagram commutes

(E) at (0,0) $\Lambda_i^{0,M}$;
[right=of E] (L) ;
[right=of L] (F) $\Lambda_j^{0,M}$,;
[above=of F] (A) $K_j^{0,M}$;
[above=of E] (D) $K_i^{0,M}$;

[->,double equal sign distance] (E)–(F) node [midway,below]$\Phi_{ij}^{\Lambda}$;
[->,double equal sign distance] (D)–(A) node [midway,above] $\Phi_{ij}^K$;
[->,double equal sign distance] (D)–(E) node [midway,left] $\Psi^i$;
[->,double equal sign distance] (A)–(F) node [midway,right] $\Psi^j$;

where $\Phi_{ij}^K$ and $\Phi_{ij}^{\Lambda}$ are the transport family-maps of
$(K^i)_{i \in I}$ and $(\Lambda^i)_{i \in I}$, respectively, according to
Definition <ref>. If $\Xi \colon(\Lambda^i)_{i \in I} \To (N^i)_{i \in I}$,
the composition $\Xi \circ \Psi \colon (K^i)_{i \in I} \To (N^i)_{i \in I}$ is defined, for every $i \in I$, by
$(\Xi \circ \Psi)^i := \Xi^i \circ \Psi^i$

(E) at (0,0) $K_i^{0,M} \ $;
[right=of E] (X) ;
[right=of X] (F) $K_j^{0,M}$;
[below=of F] (A) $ \ \Lambda_j^{0,M}$;
[left=of A] (Y) ;
[left=of Y] (B) $\Lambda_i^{0,M} \ $;
[below=of B] (K) $N_i^{0,M}$;
[right=of K] (X) ;
[right=of X] (L) $ N_j^{0,M} $.;

[->,double equal sign distance] (E)–(F) node [midway,above] $\Phi_{ij}^K$;
[->,double equal sign distance] (F)–(A) node [midway,left] $\Psi^j$;
[->,double equal sign distance] (B)–(A) node [midway,below] $\Phi_{ij}^{\Lambda}$;
[->,double equal sign distance] (E) to node [midway,right] $\Psi^i$ (B);
[->,double equal sign distance] (B) to node [midway,right] $\Xi^i$ (K);
[->,double equal sign distance] (A)–(L) node [midway,left] $\Xi^j$;
[->,double equal sign distance] (K)–(L) node [midway,below] $\Phi_{ij}^N$;
[->,double equal sign distance,bend right=40] (E) to node [midway,left] $(\Xi \circ \Psi)^i  \ $ (K);
[->,double equal sign distance,bend left=40] (F) to node [midway,right] $ \  (\Xi \circ \Psi)^j$ (L);

The identity family of families-mapidentity family of families-map$\Id_{(\Lambda^i)_{i \in I}}$
$\Id_{(\Lambda^i)_{i \in I}}$ is defined by the
rule $\big[\Id_{(\Lambda^i)_{i \in I}}\big]^i := \Id_{\Lambda_i^{0,M}}$, for every $i \in I$.
The totality of family of families-maps from $(K^i)_{i \in I}$ to $(\Lambda^i)_{i \in I}$, and
the canonical equality on $\Fam(I,M)$ is defined in analogy to Definition <ref>.

If $\Psi \colon (K^i)_{i \in I} \To (\Lambda^i)_{i \in I}$, the commutativity of the
diagram in Definition <ref> is unfolded as follows. If $i =_I j$ and $m \in \mu_0(i)$, then

\begin{align*}
\big[\Psi^j \circ \Phi_{ij}^K\big]_m = \big[\Phi_{ij}^{\Lambda} \circ \Psi^i\big]_m &
:\TOT \Psi_{\mu_{ij}(m)}^j \circ \big[\Phi_{ij}^K\big]_m = \big[\Phi_{ij}^{\Lambda}\big]_m \circ \Psi_m^i\\
& :\TOT \Psi_{\mu_{ij}(m)}^j \circ \kappa^{ij}_{m \mu_{ij}(m)} = \lambda^{ij}_{m \mu_{ij}(m)} \circ \Psi_m^i
\end{align*}

i.e., the following diagram commutes

(E) at (0,0) $\lambda_0^i(m)$;
[right=of E] (L) ;
[right=of L] (F) $\lambda^j_0(\mu_{ij}(m))$.;
[above=of F] (A) $\kappa^j_0(\mu_{ij}(m))$;
[left=of A] (M) ;
[left=of M] (D) $\kappa^i_0(m) \ $;

[->] (E)–(F) node [midway,below] $\lambda^{ij}_{m \mu_{ij}(m)}$;
[->] (D)–(A) node [midway,above] $\kappa^{ij}_{m \mu_{ij}(m)}$;
[->] (D)–(E) node [midway,left] $\Psi^i_m$;
[->] (A)–(F) node [midway,right] $\Psi^j_{\mu_{ij}(m)}$;

In analogy to Corollary <ref> we have the following.

If $(K^i)_{i \in I}, (\Lambda^i)_{i \in I}  \in \Fam(I, M)$ and
$\Psi \colon \bigcurlywedge_{i \in I}\Map\big(K_i^{0M}, \Lambda_i^{0,M}\big)$, the following are equivalent:

$\Psi \colon (K^i)_{i \in I} \To (\Lambda^i)_{i \in I} $.

$\Psi \in \prod_{i \in I}\Map\big(K_i^{0M}, \Lambda_i^{0,M}\big)$.

If $i =_I j$, the commutativity of the diagram in the definition of a family of
families-map $\Psi \colon (K^i)_{i \in I} \To (\Lambda^i)_{i \in I} $ is equivalent to
the membership condition $\Psi \in \prod_{i \in I}\Map\big(K_i^{0M}, \Lambda_i^{0,M}\big)$
using the above unfolding of the equality $\big[\Psi^j \circ \Phi_{ij}^K\big]_m =
\big[\Phi_{ij}^{\Lambda} \circ \Psi^i\big]_m$.

The totality $\prod_{i \in I}\prod_{m \in \mu_0 (i)}\lambda_0^i (m)$  of dependent functions over
a family of families of set $(\Lambda^i)_{i \in I} \in \Fam(I,M)$ is defined by

\[ \Theta \in \prod_{i \in I}\prod_{m \in \mu_0 (i)}\lambda_0^i (m) :\TOT \Theta \colon
\bigcurlywedge_{i \in I}\bigcurlywedge_{m \in \mu_0(i)}\lambda_0^i(m) \  \& \ \forall_{(i,j)
\in D(I)}\forall_{(m,n) \in T_{ij}(M)}\big(\Theta^j_n =_{\lambda^j_0(n)} \lambda^{ij}_{mn}(\Theta^i_m)\big), \]

\[ \Theta =_{\mathsmaller{\prod_{i \in I}\prod_{m \in \mu_0 (i)}\lambda_0^i (m)}} \Phi
:\TOT \forall_{i \in I}\forall_{m \in \mu_0(i)}\big(\Theta^i_m =_{\lambda_0^i(m)} \Phi^i_m\big).\]

The theory of families of families of sets over $(I,M)$ within $\D V_0^{\im}$ can be developed
further along the lines of the
theory of families of sets over $I$ within $\D V_0$.

§ NOTES

The concept of a family of sets indexed by a (discrete) set was asked to be defined
in [9], Exercise 2, p. 72, and the required definition, given by Richman,
is included in [19], Exercise 2, p. 78, where the discreteness hypothesis is omitted.
The definition has a strong type-theoretic flavour, although, Richman's motivation had categorical origin,
rather than type-theoretic. In a personal communication regarding this definition, Richman
referred to the definition of a set-indexed family of objects of a category, given in [76], p. 18,
as the source of the definition attributed to him in [19], p. 78.
Given the categorical flavour of Bishop's notion of a subset, it might be that Bishop was also
thinking in categorical terms, although Bishop, to our knowledge, neither used a purely categorical language to describe his concepts, nor he used general category theory as a foundational framework for $\BISH$.

Specifically, in [76] Richman
presented a set $I$ as a category with objects its elements and

\[ \Hom_{=_I}(i, j) := \{x \in \{0\} \mid i =_I j\}, \]

for every $i, j \in I$. If we view $\D V_0$
as a category with objects its elements and

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

for every $X, Y \in \D V_0$, then
an $I$-family of sets is a functor from the category $I$ to the category $\D V_0$.
Notice that in the definitions of $\Hom_{=_I}(i, j)$
and of $\Hom_{=_{\D V_0}}(X, Y)$ the properties $P(x) := i =_I j$ and $Q(f, f{'}) := (f, f{'}) :
X =_{\D V_0} Y$ are extensional.
In [95] we reformulated Richman's definition using the universe
$\D V_0$ of sets and the universe $\D V_1$ of triplets $(A, B, f)$, where $A, B \in \D V_0$ and $f \colon A \to B$.
Definition <ref> rests on the notion of dependent operation, in order to be absolutely
faithful to Bishop's account of sets and functions in [9] and [19].
For the definition of the concept of a family of sets in $\ZF$, or $\CZF$, see [82], p. 35, and Note <ref>.

The term “transport map” in Definition <ref> is drawn from MLTT. Actually, Definition <ref>
is a “definitional form” of the type-theoretic transport i.e., the existence of the transport map
$p_* \colon P(x) \to P(y)$, where $p \colon x =_A y$ and $P \colon A \to \C U$ is a type-family over $A \colon \C U$ in
the universe of types $\C U$.
In $\MLTT$ the existence of $p_*$ follows from Martin-Löf's $J$-rule, the induction principle that
accommodates the indentity type-family $=_A \colon A \to A \to \C U$, for every type $A \colon \C U$.
In Definition <ref> we describe in a proof-irrelevant way i.e., using only the fact that $i =_I j$ and not referring to witnesses of this equality, a structure of transport maps. This structure in $\BST$ is defined, and not generated from the equality type family of $\MLTT$.

In the categorical setting of Richman (see Note <ref>), a family map $\Psi \in \Map_I(\Lambda, M)$ is
a natural transformation from the functor $\Lambda$ to the functor $M$. The fact that the most fundamental
concepts of category theory, that of a functor and of a natural transformation, are formulated in a
natural way in $\BST$ through the notion of a dependent operation explains why category theory
is so closely connected to $\BST$. For more on the connections between $\BST$, dependent type theory and category theory see section <ref>.

The exterior union, is necessary to the definition of the infinite product of a sequence of sets.
In [19], p. 125, the following is noted:

Within the main body of this text, we have only defined the product
of a family of subsets of a given set. However, with the aid of
Problem 2 of Chapter 3 we can define the product of an arbitrary
sequence of sets. Definition (1.7) then applies to such a product[This is the
definition of the countable
product of metric spaces.].

If $\Lambda^{\Nat}$ is the sequence of sets defined in Definition <ref>,
the definitional clauses of the corresponding exterior union can be written as follows:

\[ \sum_{n \in \Nat}X_n =: \{(n, x) \mid n \in \Nat \ \& \ x \in X_n\}, \]

\[ (n, x) =_{\sum_{n \in \Nat}X_n} (m, y) : \TOT n =_{\Nat} m \ \& \ x =_{X_n} y. \]

Traditionally, the countable product of this sequence of sets is defined by

\[ \prod_{n \in \Nat}X_n := \bigg\{\phi \colon \Nat \to \sum_{n \in \Nat}X_n  \mid
\forall_{n \in \Nat}\big(\phi(n) \in X_n\big) \bigg\}, \]

which is a rough writing of the following

\[ \prod_{n \in \Nat}X_n := \bigg\{\phi \colon \Nat \to \sum_{n \in \Nat}X_n  \mid
\forall_{n \in \Nat}\big(\prb_1(\phi(n)) =_{\Nat} n\big) \bigg\}. \]

In the second writing

$\prb_1(\phi(n)) =_{\Nat} n$ implies that $\prb_1 (\phi(n) := n$,
hence, if $\phi(n) := (m, y)$, then $m = n$ and $y \in X_n$. When the equality of $I$ though, is not like
that of $\Nat$, we cannot solve this problem in a satisfying way. Although Bishop did not consider
products other than countable ones, in more  abstract areas of mathematics, like e.g., the general topology
of Bishop spaces, arbitrary products are considered (see [88]). One could have defined

\[ \Phi \in  \prod_{i \in I}\lambda_0(i) : \TOT \Phi \in \D F \bigg(I, \sum_{i \in I}\lambda_0 (i)\bigg)
\ \& \ \forall_{i \in I}\big(\prb_1(\Phi(i)) := i\big). \]

This approach has the problem that

the property

\[ Q(\Phi) : \TOT \forall_{i \in I}\big(\prb_1(\Phi(i)) := i\big) \]

is not necessarily extensional; let $\Phi =_{\mathsmaller{\D F (I, \sum_{i \in I}\lambda_0 (i))}} \Theta$ i.e.,
$\forall_{i \in I}\big(\Phi(i) =_{\mathsmaller{\sum_{i \in I}\lambda_0 (i)}} \Theta(i)\big)$, and suppose that
$Q(\Phi)$. If we fix some $i \in I$, and $\Phi(i) := (i, x)$ and $\Theta(i) := (j, y)$, we only
get that $j =_I i$. The use of dependent operations allows us to
define the right analogue to the $\prod$-type of $\MLTT$ and being at the same time compatible
with the use of dependent operations by Bishop in [9], p. 65.

A precise formulation of the definition in [19], p. 85,
of the countable product of a sequence $\big(X_n, \rho_n\big)_{n \in \Nat}$ of
metric spaces, where $\rho_n$ is bounded by $1$, for every $n \in \Nat$, is the following. Let
$\Lambda^{\Nat} := (\lambda_0^{\Nat}, \lambda_1^{\Nat})$ be the $\Nat$-family of the sets $(X_n)_{n \in \Nat}$ (see
Definition <ref>). Notice that the dependent operation $\lambda_1^{\Nat}$ is compatible to
the corresponding metric structures in the sense that each transport map $\lambda^{\Nat}_{nn} := \id_{X_n}$ is a
morphism in any category of metric spaces considered. This is an example of a spectrum of metric spaces
over $\Lambda^{\Nat}$spectrum of metric spaces over a family of sets (see also the introduction to section <ref>). The
countable product metriccountable product metric $\rho_{\infty}$$\rho_{\infty}$
on $\prod_{n \in \Nat}X_n$, for every $\Phi, \Theta \in \prod_{n \in \Nat}X_n$, is defined by

\[ \rho_{\infty}(\Phi, \Theta) := \sum_{n = 0}^{\infty}\frac{\rho_n\big(\Phi_n, \Theta_n\big)}{2^n}. \]

The equality
$ \Phi_j =_{\lambda_0 (j)} \lambda_{ij}(\Phi_i)$
in Definition <ref> is the proof-irrelevant version of dependent application of a dependent function in $\MLTT$
(see also Note <ref>).

As it is mentioned in [84], the axiom of choice is “freely used in Bishop constructivism”. In
Theorem <ref> we show only the formal version of the type-theoretic axiom choice within $\BST$ i.e., the
the distributivity of $\prod$ over $\sum$. This term was suggested to us by M. Maietti. In [95] a
proof of this result is also given, where dependecy is formulated with the help of the universe $\D V_1$
of triplets $(A, B, f)$ (see Note <ref>).
As it was first noted to us by E. Palmgren, this distributivity
holds in every locally cartesian closed category. In [131] it is mentioned that this fact
is attributed to Martin-Löf and his work [73]. For a proof see [2].

The notion of an $I$-set of sets is in accordance with Bishop's predicative spirit, and his need to avoid
the treatment of the universe $\D V_0$ as a set. This notion was not defined by Bishop, only its “internal” version, the notion
of an $I$-set of subsets, was defined similarly by him in [9], p. 65. The use of the term “set of subsets” was
a source of misreading of [9] from the side of Myhill in [80] (see also Notes <ref>
and <ref>).
The definition of the set $\lambda_0 I$ is in the spirit of the definition of the quotient group $G/H$ of the group
$G$ by its normal subgroup $H$, given in [76], p. 38.
If $I$ is equipped with the equality $=_I^{\Lambda}$, then $\Lambda$ does not become necessarily an
$I$-set of sets. The reason for this is that the transport maps of $\Lambda$ are given beforehand, and if we equip $I$
with $=_I^{\Lambda}$ we need to add a transport map $\lambda_{ij}$ for every pair $(i,j)$ for which $\lambda_0(i) =_{\D V_0}
\lambda_0(j)$ and $(i,j) \notin D(I)$, where $D(I)$ is understood here as the diagonal $D(I, =_I)$ with respect to the
equality $=_I$. So, $\lambda_1$ has to be extended, and define a new family of sets over $(I, =_I^{\Lambda})$,
which is going
to be an $(I, =_I^{\Lambda})$-set of sets.

A direct family of sets is a useful variation of the notion of a set-indexed family of sets (see Chapter <ref>).
A directed set $(I, \lt_I)$ can also be seen as
a category with objects
the elements of $I$, and $\Hom_{\lt_I}(i, j) := \{x \in \{0\} \mid i \lt_I j\}.$
If the universe $\D V_0$ is seen as a category with objects its elements and
$\Hom_{\lt_{\D V_0}}(X, Y) :=  \D F(X, Y),$ an $(I, \lt_I)$-family of sets is a
functor from the category $(I, \lt_I)$ to this new category $\D V_0$.

A generalisation of the notion of a direct family of sets is that of a preorder family of sets. If $(I, \lt_I)$ is a
preorder (see Definition <ref>), a covariant preorder family of sets
covariant preorder family of sets over $(I, \lt_I)$ is defined as a direct family of sets. One needs though the
property of a directed set to define an interesting equality on the exterior union of the corresponding family.
A contravariant preorder family of sets over $(I, \lt_I)$contravariant preorder family of sets,
or an $(I, \mt_I)$-family of
sets$(I, \mt_I)$-family of sets, is a pair
$M^{\mt} := (\mu_0, \mu_1^{\mt})$, where if $(j, i) \in D^{\mt}(I)$, the transport maps
$\mu_1^{\mt}(j, i) \colon \mu_0 (j) \to \mu_0 (i)$ behave in a dual way i.e., for every
$i, j, k \in I$ with $k \mt_I j \mt_I i$, the following diagram commutes

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

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

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

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

If $(I, \lt)$ is an inverse-directed set (see Definition <ref>) and $M^{\mt}$ is an
$(I, \mt_I)$-contravariant direct family of sets, defined in the obvious way, the
inverse-direct suminverse-direct sum $\sum_{i \in I}^{\mt} \mu_0(i)$$\sum_{i \in I}^{\mt} \mu_0(i)$
of $M^{\mt}$ is the totality $\sum_{i \in I}\mu_0(i)$, equipped with the equality

\[ (i, x) =_{\sum_{i \in I}^{\mt} \mu_0(i)} (j, y) : \TOT \exists_{k \in I}\big(i \mt_I k \
\& \ j \mt_I k \ \& \ \mu_{ik}^{\mt}(x) =_{\mu_0(k)} \mu_{jk}^{\mt}(y)\big). \]

The set $\prod_{i \in I}^{\mt}\mu_0(i)$ is defined in the expected way.
Thinking classically, a topology $T$ of
open sets on a set $X$, equipped with the subset order $\subseteq$, is an inverse-directed set, and the notion of
a presheaf of sets on $(X, T)$ is an example of a $(T, \supseteq)$-contravariant direct family of sets.
In the language of presheaves (see [65], p. 72) the transport maps $\mu_{ij}^{\mt}$ are called
restriction maps, and a family-map $\Phi \colon \Lambda^{\mt} \To M^{\mt}$ is called a morphism of presheaves.
It is natural to use also the term extension map for the transport map $\lambda_{ij}^{\lt}$ of a
covariant (direct) preorder family of sets.
The notion of a family of sets over a partial order is also used in the definition of a Kripke model
for intuitionistic predicate logic. For that see [128], p. 85, where the
transport maps $\lambda_{ij}^{\lt}$ are called there transition functions.

If a set-relevant family-map $\Psi \colon \Lambda^* \To M^*$ was defined by the stronger condition: for every $(i,j) \in D(I)$, every $p \in \varepsilon_0^{\lambda}(i,j)$ and every $q \in \varepsilon_0^{\mu}(i,j)$ the diagram in Definition <ref> commutes, then the expected fact $\id_{\Lambda^*} \colon \Lambda^* \To \Lambda^*$ implies that $\lambda_{ij}^p = \lambda_{ij}^q$, for every $p, q \in \varepsilon_0^{\lambda}(i, j)$. This property is called proof-irrelevance in Definition <ref>.

The theory of families of families of sets over $(I,M)$ within $\D V_0^{\im}$ is the third rung of the
ladder of set-like objects in $\D V_0^{\im}$.  The first three rungs can be described as follows:

\[ X, Y \in \D V_0, \ \ \ \ \ \ \ \fXY,\]

\[ \Lambda, M \in \Fam(I), \ \ \ \ \Psi \colon \Lambda \To M \TOT \Psi \in \prod_{i \in I}\D F\big(\lambda_0(i),
\mu_0(i)\big),\]

\[ (K^i)_{i \in I}, (\Lambda^i)_{i \in I} \in \Fam(I,M), \ \ \ \ \Psi \colon (K^i)_{i \in I}
\To (\Lambda^i)_{i \in I} \TOT \Psi \in \prod_{i \in I}\Map\big(K_i^{0,M}, \Lambda_i^{0,M}\big).\]

This hierarchy of universes and families can be extended further, if necessary.

[Small categories within $\BST$]
As it is mentioned in the introduction to Chapter 9 of [127], where category theory is developed within $\HoTT$, categories do not fit well with set-based mathematics. Quit earlier, see e.g, in [61],  it is mentioned that “type theory is adequate to represent faithfully categorical reasoning”. In [61] the objects are modelled as types and the Hom-sets as Hom-setoids of arrows, within the Calculus of Inductive Constructions. In [87] there are elements of such a development of category theory within type theory, where both the algebraic and the hom-definition are given. In [86] are included interesting remarks on the formulation of category theory in [127]. For relations between category theory and Explicit Mathematics see [64]. In this note we briefly explain why small categories fit well with $\BST$.

As we have already explained in Note <ref>, Richman used the notion of a functor to define the fundamental notion of a set-indexed family of sets, as a special case of a set-indexed family of objects in some category $\C C$.

Here we do the opposite. The notion of a set-indexed family of sets is fundamental and comes first.
We use the basic theory of set-indexed families of sets to describe the basic notions of category theory within $\BST$.
In what follows we consider the objects of a category to be a set, although that could also be a class. The totality of arrows
is always a set i.e., we could study locally small categories, but here we only present small categories.
A set is not  necessarily in the homotopy sense of the book-HoTT (see the corresponding notion
of a strict category in [127], section 9.6).

At this point we do not equip $\Ob_{\C C}$ with equality with evidence $(\EwE)$ that makes
possible the formulation of precategory and category in the sense of the book-HoTT (see section <ref>).

For a general discussion on the relations between categories and sets in $\BST$ see section <ref>.

A $($small$)$ categorycategory is a structure $\C C := \big(\Ob_{\C C}, \Morr^{\C C}_0,
\Morr^{\C C}_1, \Comp^{\C C}, \Id^{\C C}\big)$, where $\Ob_{\C C}$ is a set, $\big(\Morr^{\C C}_0,
\Morr^{\C C}_1\big) \in \Fam(\Ob_{\C C} \times \Ob_{\C C})$,

\[ \Comp^{\C C} : \bigcurlywedge_{x,y,z \in \Ob_{\C C}}\D F\big(\Morr^{\C C}_0(y,z) \times \Morr^{\C C}_0(x,y),
\Morr^{\C C}_0(x,z)\big),\]

\[ \Comp^{\C C}_{xyz} := \Comp^{\C C}(x,y,z) : \Morr^{\C C}_0(y,z) \times \Morr^{\C C}_0(x,y) \to
\Morr^{\C C}_0(x,z), \ \ \ \
\Comp^{\C C}_{xyz}(\phi, \psi) := \phi \circ \psi, \]

\[\Id^{\C C} : \bigcurlywedge_{x \in \Ob_{\C C}}\Morr^{\C C}_0(x,x), \ \ \ \
\Id^{\C C}_x := \Id^{\C C}(x); \ \ \ \  x \in \Ob_{\C C},\]

such that the following conditions are satisfied:

$(\Cat_1)$ For every $x, y, z, w \in \Ob_{\C C}$, $\chi \in \Morr^{\C C}_0(z, w), \phi \in \Morr^{\C C}_0(y, z)$,
$\psi \in \Morr^{\C C}_0(x, y)$,

\begin{align*}
\chi \circ (\phi \circ \psi) & := \Comp^{\C C}_{xzw}\big(\chi, \Comp^{\C C}_{xyz}(\phi, \psi)\big)\\
& =_{\mathsmaller{\Morr^{\C C}_0(x, w)}} \Comp^{\C C}_{xyw}\big(\Comp^{\C C}_{yzw}(\chi, \phi), \psi\big)\\
& := (\chi \circ \phi) \circ \psi.
\end{align*}

$(\Cat_2)$ For every $x, y \in \Ob_{\C C}$, and for every $\psi \in \Morr^{\C C}_0(x, y)$,

\[ \Id^{\C C}_y \circ \psi := \Comp^{\C C}_{xyy}(\Id^{\C C}_y, \psi)
=_{\mathsmaller{\Mor^{\C C}_0(x, y)}} \psi \ \ \ \& \ \ \
\psi \circ \Id^{\C C}_x := \Comp^{\C C}_{xxy}(\psi, \Id^{\C C}_x, \psi) =_{\mathsmaller{\Morr^{\C C}_0(x, y)}} \psi. \]

$(\Cat_3)$ For every $x, y, z, x{'}, y{'}, z{'} \in \Ob_{\C C}$, with $x =_{\mathsmaller{\Ob_{\C C}}} x{'}$,
$y =_{\mathsmaller{\Ob_{\C C}}} y{'}$ and $z =_{\mathsmaller{\Ob_{\C C}}} z{'}$, for
every $\psi \in \Morr^{\C C}_0(x, y)$,
$\phi \in \Morr^{\C C}_0(y, z)$,
$\Morr^{\C C}_{(x,z)(x{'}, z{'})}(\phi \circ \psi) =_{\mathsmaller{\Morr^{\C C}_0(x{'}, z{'})}}
\Morr^{\C C}_{(y,z)(y{'}, z{'})}(\phi) \circ \Morr^{\C C}_{(x,y)(x{'}, y{'})}(\psi)$

(E) at (0,0) $x{'}$;
[right=of E] (K) ;
[right=of K] (L) ;
[right=of L] (F) $y{'}$;
[above=of E] (D) $x$;
[right=of D] (X) ;
[right=of X] (W) ;
[right=of W] (A) $ \ y$;
[right=of A] (Y) ;
[right=of Y] (T) ;
[right=of T] (P) $ \ z$;

[right=of F] (M) ;
[right=of M] (N) ;
[right=of N] (O) $z{'}$.;

[->] (F)–(O) node [midway,above]$\Morr_{(y,z)(y{'},z{'})}(\phi)$;
[->] (E)–(F) node [midway,above]$\Morr_{(x,y)(x{'},y{'})}(\psi)$;
[->] (D)–(A) node [midway,above] $\psi$;
[->] (A)–(P) node [midway,above] $\phi$;
[-,double equal sign distance] (D)–(E) node [midway,left] ;
[-,double equal sign distance] (A)–(F) node [midway,right] ;
[-,double equal sign distance] (O)–(P) node [midway,right] ;

[->,bend right=20] (E) to node [midway,below] $\mathsmaller{\Morr^{\C C}_{(y,z)(y{'}, z{'})}(\phi)
\ \circ  \ \Morr^{\C C}_{(x,y)(x{'}, y{'})}(\psi)}$ (O);
[->,bend right=50] (E) to node [midway,below] $\mathsmaller{\Morr^{\C C}_{(x,z)(x{'}, z{'})}(\phi
\circ \psi)}$ (O);

$(\Cat_4)$ For every $x, x{'} \in \Ob_{\C C}$, with $x =_{\mathsmaller{\Ob_{\C C}}} x{'}$,
$\Morr^{\C C}_{(x,x)(x{'}, x{'})}\big(\Id^{\C C}_x\big) =_{\mathsmaller{\Morr^{\C C}_0(x{'}, x{'})}}
\Id^{\C C}_{x{'}}$

(E) at (0,0) $x{'}$;
[right=of E] (K) ;
[right=of K] (L) ;
[right=of L] (F) $x{'}$.;
[above=of F] (A) $x$;
[above=of E] (D) $x$;

[->] (E)–(F) node [midway,above]$\Morr_{(x,x)(x{'},x{'})}(\Id_x)$;
[->] (D)–(A) node [midway,above] $\Id_x$;
[-,double equal sign distance] (D)–(E) node [midway,left] ;
[-,double equal sign distance] (A)–(F) node [midway,right] ;

[->,bend right=40] (E) to node [midway,below] $\Id_{x{'}}$ (F);

The last two conditions, which reflect a functorial behaviour of the transport maps of $\Morr^{\C C}_1$ and are not
found in the standard definition of a category, are necessary
compatibility conditions between these transport maps and the $\big(\Comp^{\C C}, \Id^{\C C}\big)$-structure
of the category
$\C C$. While in intensional $\MLTT$ these conditions follow from the transport, hence the $J$-rule, here we need to include them in our definition.

As a characteristic example of a category in the above sense, we consider the constructive analogue to the category of posets.
Classically, the category of posets has objects the collection of all posets and arrows the monotone functions.
In order to formulate this constructively, we need to generalise Definition <ref> to categories with
objects an abstract totality $\Ob_{\C C}$. In Definition <ref> we define the category generated
by a spectrum of posets. We can define similarly the category generated by a spectrum of groups, rings, modules etc.
(for the notion of an $S$-spectrum, where $S$ is a structure on a set $X$, see the introduction to section <ref>).

A spectrum of posetsspectrum of posets over a set $I$ is an $I$-family of sets
$\Lambda := \big(\lambda_0, \lambda_1\big)$ such that
$(\lambda_0(i), \leq_i)$ is a poset for every $i \in I$, and for every $(i, j) \in D(I)$ the transport
map $\lambda_{ij} :
\lambda_0(i) \to \lambda_0(j)$ is a monotone function.
If $\D F^{\mon}\big(\lambda_0(i), \lambda_0(j)\big)$$F^{\mon}(X, Y)$ is the set of monotone
functions from $\lambda_0(i)$ to
$\lambda_0(j)$, the category $\C C_{\Lambda}$ generated by the $I$-spectrum $\Lambda$ is the structure
$\C C_{\Lambda} := \big(\Ob^{\C C_{\Lambda}},
\Morr_0^{\C C_{\Lambda}}, \Morr_1^{\C C_{\Lambda}}, \Comp^{\C C_{\Lambda}}, \Id^{\C C_{\Lambda}}\big)$, where
$\Ob^{\C C_{\Lambda}} :=  \lambda_0 I$, and $\Morr_0^{\C C_{\Lambda}} := \D F^{\mon}\big(\lambda_0(i), \lambda_0(j)\big)$.
If $i =_I i{'}$ and $j =_I j{'}$, and since the composition of monotone functions is monotone,  let
$\Morr^{\C C_{\Lambda}}_{(i,j)(i{'}j{'})} : \D F^{\mon}\big(\lambda_0(i), \lambda_0(j)\big) \to
\D F^{\mon}\big(\lambda_0(i{'}), \lambda_0(j{'})\big)$, defined by

\[ f \mapsto \Morr^{\C C_{\Lambda}}_{(i,j)(i{'},j{'})}(f), \ \ \ \
\Morr^{\C C_{\Lambda}}_{(i,j)(i{'},j{'})}(f) := \lambda_{jj{'}} \circ f \circ \lambda_{i{'}i}; \ \ \ \ f \in \D F^{\mon}\big(\lambda_0(i), \lambda_0(j)\big),\]

(E) at (0,0) $\lambda_0(i{'})$;
[right=of E] (H) ;
[right=of H] (F) $\lambda_0(j{'})$.;
[above=of F] (A) $\lambda_0(j)$;
[above=of E] (D) $\lambda_0(i)$;

[->] (E)–(F) node [midway,below]$\Morr^{\C C_{\Lambda}}_{(i,j)(i{'}j{'})}(f)$;
[->] (D)–(A) node [midway,above] $f$;
[->] (E)–(D) node [midway,left] $\lambda_{i{'}i}$;
[->] (A)–(F) node [midway,right] $\lambda_{jj{'}}$;

The dependent operations $\Id^{\C C_{\Lambda}}\big(\lambda_0(i)\big) := \Id_{\lambda_0(i)}$ and
$\Comp^{\C C_{\Lambda}}$ are defined as expected.

Next we only show $(\Cat_3)$ and $(\Cat_4)$ for $\C C_{\Lambda}$.
If $i =_I i{'}$, $f =_I j{'}$ and $k =_I k{'}$, we have that

\begin{align*}
\Morr^{\C C_{\Lambda}}_{(k,i)(k{'}, i{'})}(\phi) \circ \Morr^{\C C_{\Lambda}}_{(j,k)(j{'}, k{'})}(\psi) & :=
\big(\lambda_{ii{'}} \circ \phi \circ \lambda_{k{'}k} \big) \circ \big(\lambda_{kk{'}} \circ \psi \circ
\lambda_{j{'}j}\big)\\
& = \lambda_{ii{'}} \circ \phi \circ \big( \lambda_{k{'}k} \circ \lambda_{kk{'}}\big) \circ \psi \circ
\lambda_{j{'}j}\\
& = \lambda_{ii{'}} \circ (\phi \circ \psi) \circ \lambda_{j{'}j}\\
& := \Morr^{\C C_{\Lambda}}_{(j,i)(j{'}, i{'})}(\phi \circ \psi),
\end{align*}

\[ \Morr^{\C C_{\Lambda}}_{(i,i)(i{'}, i{'})}\big(\Id^{\C C_{\Lambda}}\big(\lambda_0(i)\big))
:= \Morr^{\C C_{\Lambda}}_{(i,i)(i{'}, i{'})}\big(\Id_{\lambda_0(i)}\big) := \lambda_{ii{'}} \circ \Id_{\lambda_0(i)}
\circ \lambda_{i{'}i} = \Id_{\lambda_0(j)} := \Id^{\C C_{\Lambda}}\big(\lambda_0(j)\big).\]

A functorfunctor $\B F : \C C \to \C D$ from $\C C := \big(\Ob_{\C C}, \Morr^{\C C}_0,
\Morr^{\C C}_1, \Comp^{\C C}, \Id^{\C C}\big)$ to
$\C D := \big(\Ob_{\C D}, \Morr^{\C D}_0, \Morr^{\C D}_1, \Comp^{\C D}, \Id^{\C D}\big)$ is a pair
$\B F := (F_0, F_1)$, where
$F_0 : \Ob_{\C C} \to \Ob_{\C D}$ and

\[ F_1 : \bigcurlywedge_{x, y \in \Ob_{\C C}} \D F\big(\Morr^{\C C}_0(x, y), \Morr^{\C D}_0(F_0(x), F_0(y))\big),\]

\[ F_{xy} := F_1(x,y) : \Morr^{\C C}_0(x, y) \to \Morr^{\C D}_0(F_0(x), F_0(y)), \]

such that the following conditions are satisfied:

$(\Funct_1)$ For every $x, y, z \in \Ob_{\C C}$, and for every $\psi \in \Morr^{\C C}_0(x, y)$,
$\phi \in \Morr^{\C C}_0(y, z)$ we have that

$$F_{xz}(\phi \circ \psi) =_{\mathsmaller{\Morr^{\C D}_0(F_0(x),F_0(z))}} F_{yz}(\phi) \circ F_{xy}(\psi).$$

$(\Funct_2)$ For every $x \in \Ob_{\C C}$ we have that
$F_{xx}\big(\Id^{\C C}_x\big) =_{\mathsmaller{\Morr^{\C D}_0(F_0(x),F_0(x))}} \Id^{\C D}_{F_0(x)}$.

$(\Funct_3)$ For every $x, y, x{'}, y{'} \in \Ob_{\C C}$, such that $x =_{\mathsmaller{\Ob_{\C C}}} x{'}$ and
$y =_{\mathsmaller{\Ob_{\C C}}} y{'}$, hence $(x, y) = (x{'}, y{'})$ and $\big(F_0(x), F_0(y)\big) = \big(F_0(x{'}),
F_0(y{'})\big)$, the following diagram commutes

(E) at (0,0) $\Morr^{\C D}_0(F_0(x), F_0(y))$;
[right=of E] (F) ;
[right=of F] (G) ;
[right=of G] (K) ;
[right=of K] (H) $\Morr^{\C D}_0(F_0(x{'}), F_0(y{'}))$.;
[above=of E] (A) $\Morr^{\C C}_0(x, y)$;
[above=of H] (B) $\Morr^{\C C}_0(x{'}, y{'})$;

[->] (E)–(H) node [midway,below]$\Morr^{\C D}_{\big(F_0(x), F_0(y)\big)\big(F_0(x{'}), F_0(y{'})\big)}$;
[->] (A)–(B) node [midway,above] $\Morr^{\C C}_{(x, y)(x{'}, y{'})}$;
[->] (A)–(E) node [midway,left] $F_{xy}$;
[->] (B)–(H) node [midway,right] $F_{x{'}y{'}}$;

The last condition, which is not found in the standard definition of a functor, is a compatibility condition
between the $F_1$-part of a functor $\B F : \C C \to \C D$, the transport maps $\Morr^{\C C}_1$
of $\C C$ and the transport
maps $\Morr^{\C D}_1$ of $\C D$. As an example of a standard categorical construction in this framework, we formulate the
notion of slice category. If $\C C := \big(\Ob_{\C C}, \Morr^{\C C}_0, \Morr^{\C C}_1,
\Comp^{\C C}, \Id^{\C C}\big)$ is a category and
$x \in \Ob_{\C C}$, then $\Lambda^{x} := \big(\lambda_0^x, \lambda_1^x\big) \in \Fam(\Ob_{\C C})$, where

\[ \lambda_0^x : \Ob_{\C C} \sto \D V_0, \ \ \ \ \lambda_0^x(y) :=  \Morr^{\C C}_0(y, x); \ \ \ \ y \in \Ob_{\C C},\]

\[\lambda_1^x : \bigcurlywedge_{(y, y{'}) \in D(\Ob_{\C C})}\D F\big(\Morr^{\C C}_0(y, x), \Morr^{\C C}_0(y{'}, x)\big),\]

\[\lambda^x_{yy{'}} := \lambda_1^x(y, y{'}) := \Morr^{\C C}_{(y,x)(y{'}, x)} : \Morr^{\C C}_0(y, x) \to \Morr^{\C C}_0(y{'},
x); \ \ \ \ (y,y{'}) \in \D (\Ob_{C C}).\]

Then we can prove the following fact.

Let $\C C := \big(\Ob_{\C C}, \Morr^{\C C}_0, \Morr^{\C C}_1, \Comp^{\C C}, \Id^{\C C}\big)$ be a category and
$x, z \in \Ob_{\C C}$. Let the structure $\C C/x := \big(\Ob_{\C C/x}, \Morr^{\C C/x}_0, \Morr^{\C C/x}_1, \Comp^{\C C/x},
\Id^{\C C/x}\big)$, where

\[ \Ob_{\C C/x} := \sum_{y \in \Ob_{\C C}}\lambda_0^x(y) := \sum_{y \in \Ob_{\C C}}\Morr^{\C C}_0(y, x),\]

\[\Morr^{\C C/x}_0\big((y, f), (z, g)\big) := \big\{h \in \Morr^{\C C}_0(y, z) \mid g \circ h = f\big\}.\]

If $(y, f) =_{\mathsmaller{\Ob_{\C C/x}}} (y{'}, f{'})$ and $(z, g) =_{\mathsmaller{\Ob_{\C C/x}}} (z{'}, g{'})$, the

\[ \Morr^{\C C/x}_{\big((y, f), (z, g)\big), \big((y{'}, f{'}), (z{'}, g{'})\big)} \colon
\Morr^{\C C/x}_0\big((y, f), (z, g)\big)
\to \Morr^{\C C/x}_0\big((y{'}, f{'}), (z{'}, g{'})\big), \]

\[ h \mapsto \Morr^{\C C}_{(y, z)(y{'}, z{'})}(h); \ \ \ \ h \in \Morr^{\C C/x}_0\big((y, f), (z, g)\big), \]

is well-defined. If $\Comp^{\C C/x}$
is defined in the expected compositional way, and if $\Id^{\C C/x}\big((y, f)\big)
:= \Id^{\C C}(y)$, for every $(y, f) \in \Ob_{\C C/x}$, then $\C C/x$ is a category. Moreover,
if $h \in \Morr_0^{\C C}(x,z)$, then $\B H := (H_0, H_1) \colon \C C/x \to \C C/z$, where

\[ H_0 \colon  \bigg(\sum_{y \in \Ob_{\C C}}\Morr^{\C C}_0(y, x)\bigg) \to \bigg(\sum_{y \in
\Ob_{\C C}}\Morr^{\C C}_0(y, z)\bigg), \]

\[(y, f) \mapsto (y, h \circ f); \ \ \ \ (y, f) \in \sum_{y \in \Ob_{\C C}}\Morr^{\C C}_0(y, x), \]

\[ H_1\colon \bigcurlywedge_{(y,f), (y{'}, f{'}) \in \C C/x}\D F\bigg(\Morr_0^{\C C/x}\big((y,f)(y{'},f{'})\big), \Morr_0^{\C C/z}\big((y, h \circ f),(y{'}, h \circ f{'})\big)\bigg),\]

\[ H_{(y,f)(y{'},f{'})} \colon \Morr_0^{\C C/x}\big((y,f)(y{'},f{'})\big) \to  \Morr_0^{\C C/z}\big((y, h \circ f),(y{'}, h \circ f{'})\big), \]

\[  g \mapsto g; \  \ \ \ \ g \in \Morr_0^{\C C/x}((y,f)(y{'},f{'})).\]

CHAPTER: FAMILIES OF SUBSETS

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

§ SET-INDEXED FAMILIES OF SUBSETS

Roughly speaking, a family of subsets of a set $X$ indexed by some set $I$ is an assignment routine
$\lambda_0 : I \sto \C P(X)$ that behaves like a function i.e., if $i =_I j$, then $\lambda_0(i) =_{\C P(X)}
\lambda_0 (j)$. The following definition is a formulation of this rough description that reveals the witnesses of the
equality $\lambda_0(i) =_{\C P(X)} \lambda_0 (j)$. This is done “internally”, through the embeddings of the subsets
into $X$. The equality $\lambda_0(i) =_{\D V_0} \lambda_0 (j)$, which in the previous chapter
is defined “externally” through the transport maps, follows, and a family of subsets
is also a family of sets.

Let $X$ and $I$ be sets. A family of subsetsfamily of subsets of $X$ indexed by $I$,
or an $I$-family of subsets$I$-family of subsets of $X$, is a triplet
$\Lambda(X) := (\lambda_0, \C E^X, \lambda_1)$, where
$\Lambda(X)$$\C E^X$
$\lambda_0 : I \sto \D V_0$,

\[ \C E^X : \bigcurlywedge_{i \in I}\D F\big(\lambda_0(i), X\big), \ \ \ \ \C E^X(i) := \C E_i^X; \ \ \ \ i \in I, \]

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

such that the following conditions hold:

For every $i \in I$, the function $\C E_i^X : \lambda_0(i) \to X$ is an embedding.

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

For every $(i, j) \in D(I)$ we have that
$\C E_i^X = \C E_j^X \circ \lambda_{ij}$ and $\C E_j^X = \C E_i^X \circ \lambda_{ji}$

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

[left hook->,bend left] (E) to node [midway,above] $\lambda_{ij}$ (F);
[left hook->,bend left] (F) to node [midway,below] $\lambda_{ji}$ (E);
[right hook->] (E)–(A) node [midway,left] $\C E_{i}^X \ $;
[left hook->] (F)–(A) node [midway,right] $ \ \C E_j^X$;

$\C E^X$ is a modulus of embeddingsmodulus of embeddings for $\lambda_0$, and $\lambda_1$
a modulus of transport maps for $\lambda_0$. Let
$\Lambda := (\lambda_0, \lambda_1)$ be the $I$-family of sets
that corresponds to $\Lambda(X)$the $I$-family that corresponds to $\Lambda(X)$.
If $(A, i_A) \in \C P(X)$, the constant $I$-family of subsetsconstant family of subsets
is the pair
$C^{A}(X) := (\lambda_0^{A}, \C E^{X,A}, \lambda_1^A)$, where $\lambda_0 (i) := A$, $\C E_i^{X,A} := i_A$, and
$\lambda_1 (i, j) := \id_A$, for every $i \in I$ and $(i, j) \in D(I)$ $($see the left diagram in
Definition <ref>$)$.

Let $X$ and $I$ be sets, $\lambda_0 : I \sto \D V_0$, $\C E^X$ a modulus of embeddings for $\lambda_0$, and
$\lambda_1$ a modulus of transport maps for $\lambda_0$. The following are equivalent.

$\Lambda(X) := (\lambda_0, \C E^X, \lambda_1)$ is an $I$-family of subsets of $X$.

$\Lambda := (\lambda_0, \lambda_1) \in \Fam(I)$ and $\C E^X \colon \Lambda \To C^X$, where
$C^X$ is the constant $I$-family $X$.

(i)$\To$(ii) First we show that $\Lambda \in \Fam(I)$. If $i =_I j =_I k$,
$\C E_k^X \circ (\lambda_{jk} \circ \lambda_{ij}) = (\C E_k^X \circ \lambda_{jk}) \circ \lambda_{ij}
= \C E_j^X \circ \lambda_{ij} = \C E_i^X$ and $\C E_k^X \circ \lambda_{ik} = \C E_i^X$

(E) at (0,0) $\lambda_0(i)$;
[right=of E] (B) $\lambda_0(j)$;
[right=of B] (F) $\lambda_0(k)$;
[below=of B] (C) ;
[below=of C] (A) $X$,;

[left hook->,bend left] (E) to node [midway,above] $\lambda_{ik}$ (F);
[left hook->] (E)–(B) node [midway,below] $\lambda_{ij}$ (E);
[left hook->] (B)–(F) node [midway,below] $\lambda_{jk}$ (E);
[right hook->] (E)–(A) node [midway,left] $\C E_{i}^X \ $;
[left hook->] (F)–(A) node [midway,right] $ \ \C E_k^X$;
[right hook->] (B)–(A) node [midway,left] $\C E_{j}^X  $;

hence $\C E_k^X \circ (\lambda_{jk} \circ \lambda_{ij}) = \C E_k^X \circ \lambda_{ik}$, and since $\C E_k^X$ is
an embedding, we get $\lambda_{jk} \circ \lambda_{ij} = \lambda_{ik}$. If $\C E^X \colon \Lambda \To C^X$,
the following squares are commutative

(E) at (0,0) $X$;
[right=of E] (F) $X$;
[above=of F] (A) $\lambda_0(j)$;
[above=of E] (D) $\lambda_0(i)$;
[right=of F] (G) $X$;
[above=of G] (H) $\lambda_0(j)$;
[right=of G] (K) $X$;
[above=of K] (L) $\lambda_0(i)$;

[->] (E)–(F) node [midway,below]$\id_X$;
[->] (D)–(A) node [midway,above] $\lambda_{ij}$;
[right hook->] (D)–(E) node [midway,left] $\C E_i^X$;
[left hook->] (A)–(F) node [midway,right] $\C E_j^X$;
[->] (G)–(K) node [midway,below] $\id_X$;
[->] (H)–(L) node [midway,above] $\lambda_{ji}$;
[right hook->] (H)–(G) node [midway,left] $\C E_j^X$;
[left hook->] (L)–(K) node [midway,right] $\C E_i^X$;

(E) at (0,0) ;
[right=of E] (F) $X$;
[above=of E] (A) $\lambda_0(i)$;
[right=of F] (B) ;
[above=of B] (G) $\lambda_0(j)$;
[right=of G] (K) $\lambda_0(j)$;
[below=of K] (L) ;
[right=of L] (M) $X$;
[above=of M] (N) ;
[right=of N] (P) $\lambda_0(i)$;

[right hook->] (A)–(F) node [midway,left] $\C E_i^X \ \ $;
[left hook->] (G)–(F) node [midway,right] $\ \C E_j^X$;
[right hook->] (A)–(G) node [midway,above] $\lambda_{ij}$;
[left hook->] (P)–(M) node [midway,right] $ \ \C E_i^X$;
[right hook->] (K)–(M) node [midway,left] $\C E_j^X \ \ $;
[right hook->] (K)–(P) node [midway,above] $\lambda_{ji}$;

if and only if the above triangles are commutative. The implication (ii)$\To$(i) follows immediately
from the equivalence between the commutativity of the above pairs of diagrams.

Let $X$ be a set and $(A, i_A^X), (B, i_B^X) \subseteq X$.
The triplet $\Lambda^{\D 2}(X)$$\Lambda^{\D 2}(X) := (\lambda_0^{\D 2}, \C E^X, \lambda_1^{\D 2})$,
where $\Lambda^{\D 2} := \lambda_0^{\D 2}, \lambda_1^{\D 2}$ is the $\D 2$-family of $A, B$,
$\C E^X_0 := i_A^X$, and $\C E^X_1 := i_B^X$

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

[right hook->] (A)–(F) node [midway,left] $i_A^X \ \ $;
[left hook->] (G)–(F) node [midway,right] $\ i_A^X$;
[right hook->] (A)–(G) node [midway,above] $\id_A$;
[left hook->] (P)–(M) node [midway,right] $ \ i_B^X$;
[right hook->] (K)–(M) node [midway,left] $i_B^X \ \ $;
[right hook->] (K)–(P) node [midway,above] $\id_B$;

is the $\D 2$-family of subsets $A$ and $B$$\D 2$-family of subsets of $X$.
The $\Lambda^{\D n}(X)$$\D n$-family $\Lambda^{\D n}(X)$$\Lambda^{\D n}$ of the subsets
$(A_1, i_1), \ldots, (A_n, i_n)$ of $X$$\D n$-family of subsets, and
the $\Nat$-family of subsets $(A_n, i_n)_{n \in \Nat}$$\Nat$-family of subsets of $X$
are defined similarly.

If $\Lambda(X) := (\lambda_0, \C E^X, \lambda_1), M(X) := (\mu_0, \C Z^X, \mu_1)$ and
$N(X) := (\nu_0, \C H^X, \nu_1)$ are $I$-families of subsets of $X$, a
family of subsets-mapfamily of subsets-map
$\Psi \colon \Lambda(X) \To M(X)$$\Psi \colon \Lambda(X) \To M(X)$
from $\Lambda(X)$ to $M(X)$ is a dependent operation
$\Psi : \bigcurlywedge_{i \in I}\D F\big(\lambda_0(i), \mu_0(i)\big)$, where $\Psi(i) := \Psi_i$,
for every $i \in I$, such that, for every $i \in I$, the following diagram commutes[Trivially, for
every $i \in I$ the map $\Psi_i \colon \lambda_0(i) \to \mu_0(i)$ is an embedding.]

(E) at (0,0) ;
[right=of E] (F) $X$.;
[above=of E] (A) $\lambda_0 (i)$;
[right=of F] (B) ;
[above=of B] (G) $\mu_0 (i)$;

[right hook->] (A)–(F) node [midway,left] $\C E_{i}^X \ $;
[left hook->] (G)–(F) node [midway,right] $\ \C Z_i^X$;
[right hook->] (A)–(G) node [midway,above] $\Psi_{i}$;

The totality $\Map_I(\Lambda(X), M(X))$$\Map_I(\Lambda(X), M(X))$ of family of subsets-maps
from $\Lambda(X)$ to $M(X)$ is
equipped with the pointwise equality.
If $\Psi \colon \Lambda(X) \To M(X)$ and $\Xi \colon M(X) \To N(X)$, the composition family of subsets-map
composition family of subsets-map
$\Xi \circ \Psi \colon \Lambda(X) \To N(X)$ is defined by
$(\Xi \circ \Psi)(i) := \Xi_i \circ \Psi_i$,

(E) at (0,0) $\lambda_0(i)$;
[right=of E] (B) $\mu_0(i)$;
[right=of B] (F) $\nu_0(i)$;
[below=of B] (C) $X$,;

[left hook->] (E)–(C) node [midway,left] $\C E_i \ $;
[right hook->] (B)–(C) node [midway,right] $\C Z_i$;
[right hook->] (F)–(C) node [midway,right] $ \ \C  H_{i} $;
[->] (E)–(B) node [midway,above] $\Psi_i$;
[->] (B)–(F) node [midway,above] $\Xi_i$;
[->,bend left=50] (E) to node [midway,above] $(\Xi \circ \Psi)_{i}$ (F);

for every $i \in I$. The identity family of subsets-map $\Id_{\Lambda(X)} \colon \Lambda(X) \To \Lambda(X)$
and the equality on the totality $\Fam(I,X)$$\Fam(I,X)$
of $I$-families of subsets of $X$ are defined as in Definition <ref>.

We see no obvious reason, like the one for $\Fam(I)$, not to consider
$\Fam(I, X)$ to be a set. In the case of $\Fam(I)$ the constant $I$-family $\Fam(I)$ would be in $\Fam(I)$, while
the constant $I$-family $\Fam(I, X)$ is not clear how could be seen as a family of subsets of $X$. If
$\nu_0(i) := \Fam(I, X)$, for every $i \in I$, we need to define a modulus of embeddings $\C N^X_i \colon \Fam(I, X)
\eto X$, for every $i \in I$. From the given data one could define the assignment routine $\C N^X_i$ by the rule
$\C N^X_i\big(\Lambda(X)\big) := \C E_i^X(u_i)$, if it is known that $u_i \in \lambda_0(i)$. Even in that case, the
assignment routine $\C N^X_i$ cannot be shown to satisfy the expected properties. Clearly, if $\C N^X_i$ was defined
by the rule $\C N^X_i\big(\Lambda(X)\big) := x_0 \in X$, then it cannot be an embedding.

If $\Lambda(X) M(X) \in \Fam(I, X)$, let

\[\Lambda(X) \leq M(X) :\TOT \exists_{\Phi \in \Map_I(\Lambda(X),
M(X))}\big(\Phi \colon \Lambda(X) \To M(X)\big), \]

If $\Phi \in \Map_I(\Lambda(X), M(X)), \Psi \in \Map_I(M(X), \Lambda(X)),
\Phi{'} \in \Map_I(M(X), N(X))$ and $\Psi{'} \in \Map_I(N(X), M(X))$, let the following set and operations

\[ \Eq(\Lambda(X), M(X)) := \Map_I(\Lambda(X), M(X)) \times \Map_I(M(X), \Lambda(X)), \]

\[ \refl(\Lambda) := \big(\Id_{\Lambda_X}, \Id_{\Lambda_X}\big) \ \ \& \ \ (\Phi, \Psi)^{-1} := (\Psi, \Phi) \ \ \& \ \
(\Phi, \Psi) \ast (\Phi{'}, \Psi{'}) := (\Phi{'} \circ \Phi, \Psi \circ \Psi{'}). \]

Let $\Lambda(X) := (\lambda_0, \C E^X, \lambda_1), M(X) := (\mu_0, \C Z^X, \mu_1) \in \Fam(I, X)$.

If $\Psi \colon \Lambda(X) \To M(X)$, then $\Psi \colon \Lambda \To M$.

If $\Psi \colon \Lambda(X) \To M(X)$ and $\Phi \colon \Lambda(X) \To M(X)$, then
$\Phi =_{\Map_I(\Lambda(X), M(X))} \Psi$.

(i) By the commutativity of the following inner diagrams

(m) [matrix of math nodes,row sep=3em,column sep=3em,minimum width=2em]

λ_0 (i)          μ_0 (i)

λ_0 (j)          μ_0 (j),
[left hook->]
(m-1-1) edge node [left] $\lambda_{ij}$ (m-3-1)
(m-1-1)   edge node [above] $\Psi_i$ (m-1-3);
[right hook->]
(m-1-1) edge node [right] $ \ \C E_i^X$  (m-2-2);
[left hook->]
(m-1-3) edge node [left] $\C Z_i^X \ $  (m-2-2);
[right hook->]
(m-3-1) edge node [below] $\Psi_j$ (m-3-3);
[right hook->]
(m-3-1) edge node [right] $ \ \C E_j^X$ (m-2-2);
[left hook->]
(m-3-3) edge node [left] $\C Z_j^X \ \ $ (m-2-2);
[right hook->]
(m-1-3) edge node [right] $\mu_{ij}$ (m-3-3);

we get the required commutativity of the above outer diagram.
If $x \in \lambda_0(i)$, then

\[ (\C Z_j^X \circ \Psi_j)\big(\lambda_{ij}(x)\big)
= \C E_j^X \big(\lambda_{ij}(x)\big) = \C E_i^X (x) = (\C Z_i^X \circ \Psi_i)(x) = \C Z_j^X
\big(\mu_{ij}(\Psi_i (x))\big). \]

Since $\C Z_j^X \big(\Psi_j (\lambda_{ij}(x))\big) =  \C Z_j^X
\big(\mu_{ij}(\Psi_i (x))\big)$, we get

$\Psi_j (\lambda_{ij}(x) = \mu_{ij}(\Psi_i (x))$.

(ii) If $i \in I$, then $\Psi_i \colon \lambda_0(i) \subseteq \mu_0(i)$, $\Phi_i \colon \lambda_0(i) \subseteq \mu_0(i)$

(E) at (0,0) $\lambda_0(i)$;
[right=of E] (B) ;
[right=of B] (F) $\mu_0(i)$;
[below=of B] (C) ;
[below=of C] (A) $X$,;

[left hook->,bend left] (E) to node [midway,above] $\Phi_i$ (F);
[left hook->,bend right] (E) to node [midway,below] $\Psi_i$ (F);
[right hook->] (E)–(A) node [midway,left] $\C E_i \ $;
[left hook->] (F)–(A) node [midway,right] $ \ E_i$;

hence by Proposition <ref> we get $\Psi_i =_{\D F(\lambda_0(i), \mu_0(i))} \Phi_i$.

Because of Proposition <ref>(ii) all the elements of
$\Eq(\Lambda(X), M(X))$ are equal to each other, hence the groupoid- properties (i)-(iv) for $\Eq(\Lambda(X), M(X))$
hold trivially. Of course, $\Lambda(X) =_{\Fam(I, X)} M(X) :\TOT \Lambda(X) \leq M(X) \ \& \ M(X) \leq \Lambda(X)$.
The characterisation of a family of subsets given in Proposition <ref> together with the operations
on family-maps help us define new families of subsets from given ones.

If $\Lambda(X) := (\lambda_0, \C E^X, \lambda_1) \in \Fam(I, X)$ and $M(Y) := (\mu_0, \C E^Y, \mu_1) \in \Fam(I, Y)$,

\[ (\Lambda \times M)(X \times Y) := \Lambda(X) \times M(Y) := \big(\lambda_0 \times \mu_0, \C E^X \times \C E^Y,
\lambda_1, \mu_1\big) \in \Fam(I, X \times Y),
\]

where the $I$-family $\Lambda \times M := (\lambda_0 \times \mu_0, \lambda_1 \times \mu_1)$ is defined in
Definition <ref> and the family-map $\C E^X \times \C E^Y
\colon \Lambda \times M \To C^X \times C^Y$ is defined in Proposition <ref>(ii).

By Proposition <ref>(ii) $\C E^X \times \C E^Y
\colon \Lambda \times M \To C^X \times C^Y$, where $(\C E^X \times \C E^Y)_i : \lambda_0(i) \times \mu_0(i)
\hookrightarrow X \times Y$ is defined by the rule $(u, w) \mapsto \big(\C E^X(u), \C E^Y(w)\big)$, for every
$(u, w) \in \lambda_0(i) \times \mu_0(i)$. By Proposition <ref>
this is a well-defined subset of $X \times Y$.
By Proposition <ref>(i)
$\C E^X \times \C E^Y \colon \Lambda \times M \To C^{X \times Y}$, and we use Proposition <ref>.

The operations on subsets induce operations on families of subsets.

Let $\Lambda(X) := (\lambda_0, \C E^X, \lambda_1)$ and $M(X) := (\mu_0, \C Z^X, \mu_1) \in \Fam(I, X)$.

$(\Lambda \cap M)(X) := (\lambda_0 \cap \mu_0, \C E^X \cap \C Z^X, \lambda_1 \cap \mu_1)
\in \Fam(I, X)$,$(\Lambda \cap M)(X)$
where $\lambda_0 \cap \mu_0 \colon I \sto \D V_0$ is defined by $(\lambda_0 \cap \mu_0)(i) := \lambda_0(i) \cap \mu_0(i)$,
for every $i \in I$, and the dependent operations $\C E^X \cap \C Z^X \colon
\bigcurlywedge_{i \in I}\D F\big(\lambda_0(i) \cap \mu_0(i), X\big)$,
$\lambda_1 \cap \mu_1 \colon \bigcurlywedge_{(i,j) \in D(I)}\D F\big(\lambda_0(i) \cap \mu_0(i),
\lambda_0(j) \cap \mu_0(j)\big)$ are defined by

\[ \big(\C E^X \cap \C Z^X\big)_i := i_{\lambda_0(i) \cap \mu_0(i)}^X; \ \ \ \ i \in I, \]

\[ \big[\big(\lambda_1 \cap \mu_1\big)_1(i, j)\big](u,w) := \big(\lambda_1 \cap \mu_1\big)_{ij}(u,w)
:= \big(\lambda_{ij}(u),
\mu_{ij}(w)\big); \ \ \ \ (u,w) \in \lambda_0(i) \cap \mu_0(i).
\]

$(\Lambda \cup M)(X) := (\lambda_0 \cup \mu_0, \C E^X \cup \C Z^X, \lambda_1 \cup \mu_1)
\in \Fam(I, X)$,$(\Lambda \cup M)(X)$
where $\lambda_0 \cup \mu_0 \colon I \sto \D V_0$ is defined by $(\lambda_0 \cup \mu_0)(i) := \lambda_0(i) \cup \mu_0(i)$,
for every $i \in I$, and the dependent operations $\C E^X \cup \C Z^X \colon
\bigcurlywedge_{i \in I}\D F\big(\lambda_0(i) \cup \mu_0(i), X\big)$,
$\lambda_1 \cup \mu_1 \colon \bigcurlywedge_{(i,j) \in D(I)}\D F\big(\lambda_0(i) \cup \mu_0(i),
\lambda_0(j) \cup \mu_0(j)\big)$ are defined by

\[ \big(\C E^X \cup \C Z^X\big)_i(z) := \left\{ \begin{array}{ll}
\C E_i^X(z)    &\mbox{, $z \in \lambda_0(i)$}\\
\C Z_i^X(z)             &\mbox{, $z \in \mu_0(i)$,}
\end{array}
\right.
; \ \ \ \ i \in I, \ z \in \lambda_0(i) \cup \mu_0(i) \]

\[  (\lambda_1 \cup \mu_1)_{ij}(z) := \left\{ \begin{array}{ll}
\lambda_{ij}(z)    &\mbox{, $z \in \lambda_0(i)$}\\
\mu_{ij}(z)             &\mbox{, $z \in \mu_0(i)$,}
\end{array}
\right.
; \ \ \ \ (i, j) \in D(I), \ z \in \lambda_0(i) \cup \mu_0(i). \]

(i) By Definition <ref> we have that

\[  \lambda_0(i) \cap \mu_0(i) := \{(u, w) \in \lambda_0(i) \times \mu_0(i) \mid \C E_i^X(u) =_X \C Z_i^X(w)\}, \ \ \ \
i_{\lambda_0(i) \cap \mu_0(i)}^X(u, w) := \C E_i^X(u), \]

\[ \lambda_0(j) \cap \mu_0(j) := \{(u{'}, w{'}) \in \lambda_0(j) \times \mu_0(j) \mid \C E_j^X(u{'}) =_X \C Z_j^X(w{'})\}, \
i_{\lambda_0(j) \cap \mu_0(j)}^X(u{'}, w{'}) := \C E_j^X(u{'}). \]

$\C E_j^X\big(\lambda_{ij}(u)\big) =_X \C E_i^X(u) =_X \C Z_i^X(w) =_X \C Z_j^X\big(\mu_{ij}(w)\big)$,
we get $\big(\lambda_1 \cap \mu_1\big)_{ij}(u,w) \in \lambda_0(j) \cap \mu_0(j)$.

Clearly, $\big(\lambda_1 \cap \mu_1\big)_{ij}$ is a function. The commutativity of the following left inner diagrams

(E) at (0,0) $\lambda_0(i) \cap \mu_0(i)$;
[right=of E] (B) ;
[right=of B] (F) $\lambda_0(j) \cap \mu_0(j)$;
[below=of B] (C) ;
[below=of C] (A) $X$;

[right=of F] (G) $\lambda_0(i) \cup \mu_0(i)$;
[right=of G] (H) ;
[right=of H] (J) $\lambda_0(i) \cup \mu_0(i)$;
[below=of H] (K) ;
[below=of K] (L) $X$;

[left hook->,bend left] (E) to node [midway,above] $(\lambda_1 \cap \mu_1)_{ij}$ (F);
[left hook->,bend left] (F) to node [midway,below] $(\lambda_1 \cap \mu_1)_{ji}$ (E);
[right hook->] (E)–(A) node [midway,left] $\big(\C E^X \cap \C Z^X\big)_i \ $;
[left hook->] (F)–(A) node [midway,right] $ \ \big(\C E^X \cap \C Z^X\big)_j$;

[left hook->,bend left] (G) to node [midway,above] $(\lambda_1 \cup \mu_1)_{ij}$ (J);
[left hook->,bend left] (J) to node [midway,below] $(\lambda_1 \cup \mu_1)_{ji}$ (G);
[right hook->] (G)–(L) node [midway,left] $\big(\C E^X \cup \C Z^X\big)_i \ $;
[left hook->] (J)–(L) node [midway,right] $ \ \big(\C E^X \cup \C Z^X\big)_j$;

follows by the equalities
$\big(\C E^X \cap \C X^X\big)_j\big((\lambda_1 \cap \mu_1)_{ij}(u,w)\big) :=
i_{\lambda_0(i) \cap \mu_0(i)}^X\big(\lambda_{ij}(u), \mu_{ij}(w)\big) := \C E_j^X\big(\lambda_{ij}(u)\big)
=_X \C E_i^X(u) := \big(\C E^X \cap \C X^X\big)_i(u,w)$.

(ii) First we show that $(\lambda_1 \cup \mu_1)_{ij}$ is a function. The more interesting case is $z \in \lambda_0(i)$,
$w \in \mu_0(i)$ and $\C E_i^X(z) =_X \C Z_i^X(w)$. Hence $\C E_j^X\big(\lambda_{ij}(u)\big) =_X =_X
\C Z_j^X\big(\mu_{ij}(w)\big)$, and $\lambda_{ij}(z) =_{\mathsmaller{\lambda_0(i) \cup \mu_0(i)}} \mu_{ij}(w)$.
The commutativity of the above right inner diagrams is straightforward to show.

Let $\Lambda(X) := (\lambda_0, \C E^X, \lambda_1) \in \Fam(I, X)$ and $M(Y) := (\mu_0, \C E^Y, \mu_1) \in \Fam(J, Y)$.
If $\fXY$, let

$[f(\Lambda)](Y) := \big(f(\lambda_0), f(\C E^X)^Y, f(\lambda_1)\big)$[$f(\Lambda)](Y)$, where
the non-dependent assignment routine $f(\lambda_0) \colon I \sto \D V_0$, and the
dependent operations $f(\C E^X)^Y \colon \bigcurlywedge_{i \in I}
\D F(f(\lambda_0)(i), Y)$ and $f(\lambda_1) \colon \bigcurlywedge_{(i, i{'}) \in D(I)}\D F\big(f(\lambda_0)(i),
f(\lambda_0)(i{'})\big)$ are defined by

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

[right hook->] (E)–(F) node [midway,above] $\C E_i^X$;
[->] (F)–(A) node [midway,above] $f$;
[->,bend right] (E) to node [midway,below] $f_i^Y$ (A);

\[ [f(\lambda_0)](i) := f(\lambda_0(i)) := (\lambda_0(i), f_i), \ \ \ \ f_i^Y := f \circ \C E_i^X; \ \ \ \ i \in I, \]

\[ \big[f(\C E^X)^Y\big](i) := f_i^Y, \ \ \ \  f(\lambda_1)_{ii{'}} := \lambda_{ii{'}};  \ \ \ \ i \in I, \ (i, i{'}) \in D(I). \]

We call $[f(\Lambda)](Y)$ the image of $\Lambda$image of a family of subsets under $f$.
The pre-image of $M$pre-image of a family of subsets under $f$ is the triplet
$[f^{-1}(M)](X) := \big(f^{-1}(\mu_0), f^{-1}(\C E^Y)^X, f^{-1}(\mu_1)\big)$[$f^{-1}(M)](X)$, where
the non-dependent assignment routine $f^{-1}(\mu_0) \colon J \sto \D V_0$, and the
dependent operations $f^{-1}(\C E^Y)^X \colon \bigcurlywedge_{j \in J}
\D F(f^{-1}(\mu_0)(j), X)$ and $f^{-1}(\mu_1) \colon \bigcurlywedge_{(j, j{'}) \in D(J)}\D F\big(f^{-1}(\mu_0)(j),
f^{-1}(\mu_0)(j{'})\big)$ are defined by

\[ [f^{-1}(\mu_0)](j) := f^{-1}(\mu_0(j)) := \big\{(x, y) \in X \times \mu_0(j) \mid f(x) =_Y \C E_j^Y(y)\big\};
\ \ \ \ j \in J \]

\[ e_j \colon f^{-1}(\mu_0(j)) \eto X \ \ \ \ e_j(x, y) := x; \ \ \ \ x \in X, \ y \in \mu_0(j), \ j \in
J, \]

\[ \big[f^{-1}(\C E^Y)^X\big](j) := e_j; \ \ \ \ j \in J, \]

\[ f^{-1}(\mu_1)_{jj{'}} \colon f^{-1}(\mu_0)(j) \to f^{-1}(\mu_0)(j{'}) \ \ \ \ f^{-1}(\mu_1)_{jj{'}}(x, y) :=
(x, \mu_{jj{'}}(y)); \ \ \ \ (j, j{'}) \in D(J). \]

Then $[f(\Lambda)](Y) \in \Fam(I, Y)$ and $[f^{-1}(M)](X) \in \Fam(J, X)$.

It suffices to show the commutativity of the following diagrams

(E) at (0,0) $\lambda_0(i)$;
[right=of E] (B) ;
[right=of B] (F) $\lambda_0(i{'})$;
[below=of B] (C) ;
[below=of C] (A) $X$;
[left=of A] (D) $Y$;

[right=of F] (G) $f^{-1}(\mu_0)(j)$;
[right=of G] (H) ;
[right=of H] (J) $f^{-1}(\mu_0)(j{'})$;
[below=of H] (K) ;
[below=of K] (L) $X$.;

[left hook->,bend left] (E) to node [midway,above] $\lambda_{ii{'}}$ (F);
[left hook->,bend left] (F) to node [midway,below] $\lambda_{i{'}i}$ (E);
[right hook->] (E)–(A) node [midway,left] $\C E_i^X \ $;
[left hook->] (F)–(A) node [midway,right] $ \ \C E^X_{i{'}}$;
[->] (A)–(D) node [midway,above] $f$;
[left hook->,bend left] (G) to node [midway,above] $f^{-1}(\mu_1)_{jj{'}}$ (J);
[left hook->,bend left] (J) to node [midway,below] $f^{-1}(\mu_1)_{j{'}j}$ (G);
[right hook->] (G)–(L) node [midway,left] $\mathsmaller{\big[f^{-1}(\C E^Y)^X\big](j)} \ $;
[left hook->] (J)–(L) node [midway,right] $ \ \mathsmaller{\big[f^{-1}(\C E^Y)^X\big](j{'})}$;

For the left, we use the supposed commutativity of the two diagrams without the arrow $\fXY$. For the above right
outer diagram we have that $\big[f^{-1}(\C E^Y)^X\big](j{'})\big(f^{-1}(\mu_1)_{jj{'}}(x, y)\big) :=
\big[f^{-1}(\C E^Y)^X\big](j{'})(x, \mu_{jj{'}}(y)) := e_{j{'}}((x, \mu_{jj{'}}(y)) := x := e_j(x, y) :=
\big[f^{-1}(\C E^Y)^X\big](j)(x, y)$. For the commutativity of the above right inner diagram we proceed similarly.

The operations on families of subsets generate operations on family of subsets-maps.

Let $\Lambda(X), K(X), M(X), N(X) \in \Fam(I, X)$, $P(Y), Q(Y) \in \Fam(J, Y)$, and $\fXY$.
Let also $\Phi \colon \Lambda(X) \To K(X)$, $\Psi \colon M(X) \To N(X)$, and $\Xi \colon P(Y) \To Q(Y)$.

$\Phi \cap \Psi \colon (\Lambda \cap M)(X) \To (K \cap N)(X)$, where, for every $i \in I$ and
$(u,w) \in \lambda_0(i) \cap \mu_0(i)$,

\[ (\Phi \cap \Psi)_i \colon \lambda_0(i) \cap \mu_0(i) \to k_0(i) \cap \nu_0(i), \ \ \ \
(\Phi \cap \Psi)_i(u,w) := \big(\Phi_i(u), \Psi_i(w)\big). \]

$\Phi \cup \Psi \colon (\Lambda \cup M)(X) \To (K \cup N)(X)$, where, for every $i \in I$,

\[ (\Phi \cup \Psi)_i \colon \lambda_0(i) \cup \mu_0(i) \to k_0(i) \cup \nu_0(i), \]

\[  (\Phi \cup \Psi)_i(z) := \left\{ \begin{array}{ll}
\Phi_i(z)    &\mbox{, $z \in \lambda_0(i)$}\\
\Psi_i(z)             &\mbox{, $z \in \mu_0(i)$}
\end{array}
\right.
\]

$\Phi \times \Xi \colon (\Lambda \times P)(X \times Y) \To (K \times Q)(X \times Y)$, where,
for every $i \in I$ and
$(u,w) \in \lambda_0(i) \times p_0(i)$,

\[ (\Phi \times \Xi)_i \colon \lambda_0(i) \times p_0(i) \to k_0(i) \times q_0(i), \ \ \ \
(\Phi \times \Xi)_i(u,w) := \big(\Phi_i(u), \Xi_i(w)\big). \]

$f(\Phi) \colon [f(\Lambda)](Y) \To [f(K)](Y)$, where,
for every $i \in I$ and $u \in f(\lambda_0(i))$,

\[ [f(\Phi)]_i \colon f(\lambda_0(i)) \to f(k_0(i)), \ \ \ \
[f(\Phi)]_i(u) := \Phi_i(u). \]

$f^{-1}(\Xi) \colon [f^{-1}(P)](X) \To [f^{-1}(Q)](X)$, where,
for every $j \in J$ and $(x,y) \in f^{-1}(p_0(j))$,

\[ [f^{-1}(\Xi)]_i \colon f^{-1}(p_0(j)) \to f^{-1}(q_0(j)), \ \ \ \
[f^{-1}(\Xi)]_j(x, y) := \big(x, \Xi_j(y)\big). \]

It is straightforward to show that all family of subsets-maps above are well-defined.

Let $\Lambda(X) := (\lambda_0, \C E^X, \lambda_1) \in \Fam(I, X)$ and $h \colon J \to I$. The triplet
$\Lambda(X) \circ h := (\lambda_0 \circ h, \C E^X \circ h, \lambda_1 \circ h)$, where $\Lambda \circ h :=
(\lambda_0 \circ h, \lambda_1 \circ h)$ is the $h$-subfamily of $\Lambda$, and the dependent operation
$\C E^X \circ h \colon \bigcurlywedge_{j \in J}\D F\big(\lambda_0(h(j)), X\big)$ is defined by
$(\C E^X \circ h)_j := \C E^X_{h(j)}$, for every $j \in J$, is called the $h$-subfamily of $\Lambda(X)$$h$-subfamily of a family of subsets. If $J := \Nat$, we call $\Lambda(X) \circ h$ the $h$-subsequence of $\Lambda(X)$$h$-subsequence of $\Lambda(X)$.

It is immediate to show that $\Lambda(X) \circ h \in \Fam(J, X)$, and if $\Lambda(X) \circ h \in \Set(J, X)$,
then $h$ is an embedding. All notions and results of section <ref> on
subfamilies of families of sets extend naturally to subfamilies of families of subsets.

§ THE INTERIOR UNION OF A FAMILY OF SUBSETS

Let $\Lambda(X) := (\lambda_0, \C E^X, \lambda_1)$ be an $I$-family of subsets of $X$.
The interior unioninterior union, or simply the unionunion of a family of subsets
of $\Lambda(X)$ is the totality $\sum_{i \in I} \lambda_0(i)$, which we
denote in this case by $\bigcup_{i \in I} \lambda_0(i)$.
Let the non-dependent assignment routine
$e_{\mathsmaller{\bigcup}}^{\Lambda(X)} \colon \bigcup_{i \in I} \lambda_0(i) \sto X$ defined by
$(i, x) \mapsto \C E_i^X (x)$, for every $(i, x) \in \bigcup_{i \in I} \lambda_0(i)$, and let

\[ (i, x) =_{\mathsmaller{\bigcup_{i \in I} \lambda_0(i)}} (j, y) :\Leftrightarrow
e_{\mathsmaller{\bigcup}}^{\Lambda(X)}(i, x) =_X
e_{\mathsmaller{\bigcup}}^{\Lambda(X)}(j, y) :\Leftrightarrow \C E_i^X (x) =_X \C E_j^X (y). \]

If $\neq_X$ is an inequality on $X$, let
$(i, x) \neq_{\mathsmaller{\bigcup_{i \in I} \lambda_0(i)}} (j, y) :\Leftrightarrow
\C E_i^X (x) \neq_X \C E_j^X (y)$.

The family $\Lambda(X)$ is called a coveringcovering of $X$, or
$\Lambda(X)$ covers $X$$\Lambda(X)$ covers $X$,  if

\[ \bigcup_{i \in I} \lambda_0(i)  =_{\C P (X)} X. \]

If $\neq_I$ is an inequality on $I$, and $\neq_X$ an inequality on $X$, we say that $\Lambda(X)$ is a
family of disjoint subsets of $X$family of disjoint subsets of $X$ $($with respect to $\neq_I)$,  if

\[ \forall_{i, j \in I}\big(i \neq_I j \To \lambda_0(i) \Disj \lambda_0(j)\big), \]

where by Definition <ref>
$\lambda_0(i) \Disj \lambda_0(j) :\TOT \forall_{u \in \lambda_0(i)}\forall_{w \in
\lambda_0(j)}\big(\C E_i^X(u) \neq_X \C E_j^X(w)\big)$.

$\Lambda(X)$ is called a partitionpartition of $X$, if it covers $X$ and
it is a family of disjoint subsets of $X$.

Clearly, $=_{\mathsmaller{\bigcup_{i \in I} \lambda_0(i)}}$ is an equality on
$\bigcup_{i \in I} \lambda_0(i)$, which is considered to be a set, and the
operation $e_{\mathsmaller{\bigcup}}^{\Lambda(X)}$
is an embedding of $\bigcup_{i \in I} \lambda_0(i)$ into $X$, hence
$\big(\bigcup_{i \in I} \lambda_0(i), e_{\mathsmaller{\bigcup}}^{\Lambda(X)}\big) \subseteq X$. The inequality
$\neq_{\mathsmaller{\bigcup_{i \in I} \lambda_0(i)}}$ is the canonical inequality of the subset
$\bigcup_{i \in I} \lambda_0(i)$ of $X$ (see Corollary <ref>).
Hence, if $(X, =_X, \neq_X)$ is discrete, then $\big(\bigcup_{i \in I} \lambda_0(i),
=_{\mathsmaller{\bigcup_{i \in I} \lambda_0(i)}}, \neq_{\mathsmaller{\bigcup_{i \in I} \lambda_0(i)}}\big)$ is discrete,
and if $\neq_X$ is tight, then $=_{\mathsmaller{\bigcup_{i \in I} \lambda_0(i)}}$ is tight.
As the following left diagram commutes, $\Lambda(X)$ covers $X$, if and only of the following right
diagram commutes i.e., if and only if $X \subseteq \bigcup_{i \in I} \lambda_0(i)$

(E) at (0,0) $\bigcup_{i \in I} \lambda_0(i)$;
[right=of E] (B) ;
[right=of B] (F) $X$;
[below=of B] (C) ;
[below=of C] (A) $X$;

[right=of F] (G) $\bigcup_{i \in I} \lambda_0(i)$;
[right=of G] (H) ;
[right=of H] (J) $X$;
[below=of H] (K) ;
[below=of K] (L) $X$.;

[left hook->,bend left] (E) to node [midway,above] $e_{\mathsmaller{\bigcup}}^{\Lambda(X)}$ (F);

[right hook->] (E)–(A) node [midway,left] $e_{\mathsmaller{\bigcup}}^{\Lambda(X)} \ $;
[left hook->] (F)–(A) node [midway,right] $ \ \id_X$;

[right hook->,bend right] (J) to node [midway,above] $g$ (G);

[right hook->] (G)–(L) node [midway,left] $e_{\mathsmaller{\bigcup}}^{\Lambda(X)} \ $;
[left hook->] (J)–(L) node [midway,right] $ \ \id_X$;

If $(i, x) =_{\mathsmaller{\bigcup_{i \in I} \lambda_0(i)}} (j, y)$, it is not
necessary that $i =_I j$, hence it is not necessary that
$(i, x) =_{\mathsmaller{\sum_{i \in I} \lambda_0(i)}} (j, y)$ (as we show in the next proposition, the converse
implication holds). Consequently, the first projection operation $\pr_1^{\Lambda(X)}
:= \pr_1^{\Lambda}$$\pr_1^{\Lambda(X)}$, where $\Lambda$ is the $I$-family of sets induced by $\Lambda(X)$,

is not necessarily a function!
The second projection map on $\Lambda(X)$ is defined by
$\pr_2^{\Lambda(X)} := \pr_2^{\Lambda}$$\pr_2^{\Lambda(X)}$.
Notice that $\neq_{\mathsmaller{\bigcup_{i \in I} \lambda_0(i)}}$ is an
inequality on $\bigcup_{i \in I} \lambda_0(i)$, without supposing neither an inequality on $I$, nor an inequality
on the sets $\lambda_0(i)$'s, as we did in Proposition <ref>(ii).
Moreover, $\neq_{\mathsmaller{\bigcup_{i \in I}}}$ is tight, if $\neq_X$ is tight. Cases (ii) and (iii) of the next
proposition are due to M. ZeunerZeuner.

Let $\Lambda(X) := (\lambda_0, \C E^X, \lambda_1) \in \Fam(I, X)$.

If $(i, x) =_{\mathsmaller{\sum_{i \in I} \lambda_0(i)}} (j, y)$, then
$(i, x) =_{\mathsmaller{\bigcup_{i \in I} \lambda_0(i)}} (j, y)$.

If $e_{\mathsmaller{\bigcup}}^{\Lambda(X)} \colon \sum_{i \in I} \lambda_0(i) \sto X$ is an embedding,

$\big(\sum_{i \in I} \lambda_0(i), e_{\mathsmaller{\bigcup}}^{\Lambda(X)}\big) =_{\C P(X)} \big(\bigcup_{i \in I} \lambda_0(i), e_{\mathsmaller{\bigcup}}^{\Lambda(X)}\big)$.

If $\neq_I$ is a tight inequality on $X$, and $\Lambda(X)$ is a family of disjoint subsets of $X$
with respect to $\neq_I$, then  $e_{\mathsmaller{\bigcup}}^{\Lambda(X)} \colon \sum_{i \in I} \lambda_0(i) \eto X$.

(i) If $i =_I j$, and since $\C E_j^X$ is a function, we get
$\C E_i^X(x) = \C E_j^X(\lambda_{ij}(x)) = \C E_j^X(y)$.

(ii) Let $\C E_i^X(x) =_X \C E_j^X(y) \TOT (i, x) =_{\mathsmaller{\sum_{i \in I}\lambda_0(i)}} (j, y)$.
We define the operations $\id_1 \colon \sum_{i \in I}\lambda_0(i) \sto \bigcup_{i \in I}\lambda_0(i)$ and
$\id_2 \colon \bigcup_{i \in I}\lambda_0(i) \sto \sum_{i \in I}\lambda_0(i)$, both
defined by the identity map-rule. That $\id_1$ is a function, follows from (i).
That $\id_2$ is a function, follows from the hypothesis on  $e_{\mathsmaller{\bigcup}}^{\Lambda(X)}$.

(iii) We suppose that $e_{\mathsmaller{\bigcup}}^{\Lambda(X)}(i, x) := \C E_i^X(x) =_X \C E_j^X(y)
:= e_{\mathsmaller{\bigcup}}^{\Lambda(X)}(j, y)$ and we show that
$(i,x) =_{\mathsmaller{\sum_{i \in I}\lambda_0(i)}} (j, y)$. The converse implication follows from (i).
If $\neg(i \neq_I j)$, then $\lambda_0(i) \Disj \lambda_0(j)$, hence
$\C E_i^X(x) \neq_X \C E_j^X(y)$, which contradicts our hypothesis. By the tightness of $\neq_I$ we
get $i =_I j$, and it remains to show that $\lambda_{ij}(x) =_{\mathsmaller{\lambda_0(j)}} y$. By
the equalities $\C E_j^X\big(\lambda_{ij}(x)\big) =_X \C E_i^X(y) =_X \C E_j^X(y)$, and as $\C E_j^X$
is an embedding, we get $\lambda_{ij}(x) =_{\mathsmaller{\lambda_0(j)}} y$.

Let $i_0 \in I$, $(A, i_A^X) \subseteq X$, and $C^A(X) := (\lambda_0^A, \C E^{A, X}, \lambda_1^A)
\in \Fam(I, X)$ the constant family $A$ of subsets of $X$. Then

\[ \bigcup_{i \in I}A := \bigcup_{i \in I}\lambda_0^A(i) =_{\C P(X)} A. \]

By definition $(i, a) =_{\mathsmaller{\bigcup_{i \in I}A}} (j, b) :\TOT \C E^{A,X}_i(a) =_X \C E^{A,X}_j(b) :\TOT
i_A^X(a) =_X i_A^X(b) \TOT a =_A b$. Let the operation $\phi \colon \bigcup_{i \in I}A \sto A$, defined by
$\phi(i, a) := a$, for every $(i, a) \in \bigcup_{i \in I}A$, and let the operation
$\theta \colon A \sto \bigcup_{i \in I}A$, defined by $\theta(a) := (i_0, a)$, for every
$a \in A$. Clearly, $\phi$ and $\theta$ are functions. The required equality of these subsets
follows from the following equalities:
$i_A^X(a) =_X e^{C^A(X)}_{\mathsmaller{\bigcup}}(i, a) := \C E^{A, X}_i(a) := i_A^X(a)$,
and $e^{C^A(X)}_{\mathsmaller{\bigcup}}(i_0, a) := \C E^{A, X}_{i_0}(a) := i_A^X(a)$.

The interior union of a family of subsets generalises the union of two subsets.

If $\Lambda^{\D 2}(X)$ is the $\D 2$-family of subsets $A, B$ of $X$,

$\bigcup_{i \in \D 2} \lambda_0^{\D 2}(i) =_{\C P(X)} A \cup B.$

The operation $g \colon \bigcup_{i \in \D 2}\lambda_0^{\D 2} (i) \sto A \cup B$, defined by $g(i, x) := \prb_2 (i, x)
:= x$, for every $(i, x) \in \bigcup_{i \in \D 2}\lambda_0^{\D 2} (i)$, is well-defined, and it is an embedding,
$ g(i, x) =_{A \cup B} g(j, y) :\TOT x =_{A \cup B} y
:\TOT i^X_A(x) =_X i^X_B(y)
%:\TOT e(i, x) =_X e(j, y)
:\TOT (i, x) =_{\mathsmaller{\bigcup_{i \in \D 2}\lambda_0 (i)}} (j, y).

The operation $f : A \cup B \sto \bigcup_{i \in \D 2}\lambda_0^{\D 2} (i)$, defined by
$f(z) := (0,z)$, if $z \in A$, and $f(z) := (1, z)$, if $z \in B$,

is easily seen to be a function. For the commutativity of the following inner diagrams

(E) at (0,0) $A \cup B$;
[right=of E] (B) ;
[right=of B] (F) $\mathsmaller{\bigcup_{i \in \D 2} \lambda_0^{\D 2}(i)}$;
[below=of B] (C) ;
[below=of C] (A) $X$;

[left hook->,bend left] (E) to node [midway,above] $f$ (F);
[left hook->,bend left] (F) to node [midway,below] $g$ (E);
[right hook->] (E)–(A) node [midway,left] $i_{A \cup B}^X \ $;
[left hook->] (F)–(A) node [midway,right] $ \ e_{\mathsmaller{\bigcup}}^{\Lambda^{\D 2}(X)}$;

we use the equalities $i_{A \cup B}^X(g(i, x)) := i_{A \cup B}^X(x) := i_A^X(x)
:= e_{\mathsmaller{\bigcup}}^{\Lambda^{\D2}(X)}(i, x)$ and

\[ e_{\mathsmaller{\bigcup}}^{\Lambda^{\D 2}(X)}f(z)) := \left\{ \begin{array}{lll}
e_{\mathsmaller{\bigcup}}^{\Lambda^{\D 2}(X)}(0, z)    &\mbox{, $z \in A$}\\
e_{\mathsmaller{\bigcup}}^{\Lambda^{\D 2}(X)}(1, z)             &\mbox{, $z \in B$}
\end{array}
\right.
%           := \left\{ \begin{array}{ll}
%                  e_{\mathsmaller{\bigcup}}^X(0, z)    &\mbox{, $z \in A$}\\
%                  e_{\mathsmaller{\bigcup}}^X(1, z)             &\mbox{, $z \in B$}
%                  \end{array}
%                  \right.
:= \left\{ \begin{array}{lll}
i_A^X(z)    &\mbox{, $z \in A$}\\
i_B^X(z)             &\mbox{, $z \in B$}
\end{array}
\right.
:= i_{A \cup B}^X(z).\qedhere \]

Let $\Lambda(X) := (\lambda_0, \C E^X, \lambda_1) \in \Fam(I, X)$ and $M(Y) := (\mu_0, \C E^Y, \mu_1) \in \Fam(I, Y)$.
If $\fXY$, the following hold:

$f \bigg(\bigcup_{i \in I} \lambda_0(i)\bigg) =_{\C P(Y)} \bigcup_{i \in I} f\big(\lambda_0(i)\big)$.

$f^{-1} \bigg(\bigcup_{i \in I} \mu_0(i)\bigg) =_{\C P(X)} \bigcup_{i \in I} f^{-1}\big(\mu_0(i)\big)$.

(i) By Definition <ref> we have that $f\big(\bigcup_{i \in I} \lambda_0(i)\big) :=
\big(\bigcup_{i \in I} \lambda_0(i), f_{\mathsmaller{\bigcup}}^{\Lambda(X)}\big)$,
where $f_{\mathsmaller{\bigcup}}^{\Lambda(X)} := f \circ e_{\mathsmaller{\bigcup}}^{\Lambda(X)}$,
and by Proposition <ref> we have that

\begin{align*}
(i,x) =_{\mathsmaller{f\big(\bigcup_{i \in I} \lambda_0(i)\big)}} (j,y)
& :\TOT f_{\mathsmaller{\bigcup}}^{\Lambda(X)}(i,x) =_Y  f_{\mathsmaller{\bigcup}}^{\Lambda(X)}(j,y)\\
& :\TOT \big(f \circ e_{\mathsmaller{\bigcup}}^{\Lambda(X)}\big)(i,x) =_Y
\big(f \circ e_{\mathsmaller{\bigcup}}^{\Lambda(X)}\big)(j,y)\\
& :\TOT f\big(\C E_i^X(x)\big) =_Y f\big(\C E_j^X(y)\big)\\
& :\TOT f_i^Y(x) =_Y f_j^Y(y)
\end{align*}

By Proposition <ref> and Definition <ref> for the subset
$\big(\bigcup_{i \in I} f\big(\lambda_0(i)\big), e_{\mathsmaller{\bigcup}}^{[f(\Lambda)](Y)}\big)$ of $Y$ we have that
$f(\lambda_0(i)) := \big(\lambda_0(i), f_i^Y\big)$, where $f_i^Y := f \circ \C E_i^X$, for every $i \in I$, and
$x =_{\mathsmaller{f(\lambda_0(i))}} x{'} :\TOT f_i^Y(x) =_Y f_o^Y(x{'})$.
Moreover, $e_{\mathsmaller{\bigcup}}^{[f(\Lambda)](Y)}(i,x)
:= \big[f(\C E^X)^Y\big]_i(x) := f_i^Y(x)$. Let the operations $g \colon f\big(\bigcup_{i \in I} \lambda_0(i)\big)
\sto \bigcup_{i \in I} f\big(\lambda_0(i)\big)$ and $h \colon \bigcup_{i \in I} f\big(\lambda_0(i)\big) \sto
f\big(\bigcup_{i \in I} \lambda_0(i)\big)$, defined by the same rule $(i,x) \mapsto (i,x)$.

(E) at (0,0) $\mathsmaller{f\big(\bigcup_{i \in I} \lambda_0(i)\big)}$;
[right=of E] (B) ;
[right=of B] (F) $\mathsmaller{\bigcup_{i \in I} f\big(\lambda_0(i)\big)}$;
[below=of B] (C) ;
[below=of C] (A) $X$;

[right=of F] (G) $\mathsmaller{f^{-1} \big(\bigcup_{i \in I} \mu_0(i)\big)}$;
[right=of G] (H) ;
[right=of H] (J) $\bigcup_{i \in I} f^{-1}\big(\mu_0(i)\big)$;
[below=of H] (K) ;
[below=of K] (L) $X$;

[left hook->,bend left] (E) to node [midway,above] $g$ (F);
[left hook->,bend left] (F) to node [midway,below] $h$ (E);
[right hook->] (E)–(A) node [midway,left] $f_{\mathsmaller{\bigcup}}^{\Lambda(X)} \ $;
[left hook->] (F)–(A) node [midway,right] $ \ \mathsmaller{\big[f^{-1}(\C E^Y)^X\big](j{'})}$;

[left hook->,bend left] (G) to node [midway,above] $g{'}$ (J);
[left hook->,bend left] (J) to node [midway,below] $h{'}$ (G);
[right hook->] (G)–(L) node [midway,left] $e_{\mathsmaller{\bigcup}}^{[f^{-1}(M)](X)} \ $;
[left hook->] (J)–(L) node [midway,right] $ \ \mathsmaller{\big[f^{-1}(\C E^Y)^X\big]_i}$;

It is immediate by the previous equalities that the above left diagrams commute.

(ii) By Definitions <ref> and <ref> for the subset
$\big(\bigcup_{i \in I} \mu_0(i), e_{\mathsmaller{\bigcup}}^{M(Y)}\big)$ of $Y$ we have that the embedding
$e_{\mathsmaller{\bigcup}}^{M(Y)} \colon \bigcup_{i \in I} \mu_0(i) \eto Y$ is given
by the rule $(i,y) \mapsto \C E_i^Y(y)$, and

\[ f^{-1} \bigg(\bigcup_{i \in I} \mu_0(i)\bigg) := \bigg\{\big(x, (i,y)\big) \in X \times \bigcup_{i \in I} \mu_0(i)
\mid f(x) =_Y e_{\mathsmaller{\bigcup}}^{M(Y)}(i,y) \bigg\}, \]

with embedding into $X$ the mapping $e^X$, defined by the rule $e^X\big(x, (i,y)\big) := x$. Moreover,

\[ \big(x, (i,y)\big) =_{\mathsmaller{f^{-1}(\bigcup_{i \in I} \mu_0(i))}}
\big(x{'}, (i{'},y{'})\big) :\TOT x =_X x{'} \ \& \ \C E_i^Y(y) =_Y \C E_{i{'}}^Y(y{'}). \]

The subset $f^{-1}(\mu_0(i)) := \{(x,y) \in X \times \mu_0(i) \mid f(x) =_Y \C E_i^Y(y)\}$ of $X$ is equipped with
the embedding $e^X_{\mathsmaller{f^{-1}(\mu_0(i))}} \colon f^{-1}(\mu_0(i)) \eto X$, which is defined by
$e^X_{\mathsmaller{f^{-1}(\mu_0(i))}}(x, y) := x$, for every $(x,y) \in f^{-1}(\mu_0(i))$. Moreover, we have that

\begin{align*}
\big(x, (i,y)\big) =_{\mathsmaller{\bigcup_{i \in I} f^{-1}\big(\mu_0(i)\big)}}
\big(x{'}, (i{'},y{'})\big) & :\TOT \big[f^{-1}(\C E^Y)^X\big]_i(x,y) =_X \big[f^{-1}(\C E^Y)^X\big]_{i{'}}(x{'},y{'})\\
& :\TOT e_{\mathsmaller{f^{-1}(\mu_0(i))}}^X(x,y) =_X f^{-1}(\mu_0(i{'}))(x{'},y{'})\\
& :\TOT x =_X x{'}.
\end{align*}

If the operation $g{'} \colon f^{-1} \big(\bigcup_{i \in I} \mu_0(i)\big) \sto \bigcup_{i \in I} f^{-1}\big(\mu_0(i)\big)$
is defined by the rule $\big(x, (i,y)\big) \mapsto \big(i, (x,y)\big)$ and the operation
$h{'} \colon  \bigcup_{i \in I} f^{-1}\big(\mu_0(i)\big) \sto f^{-1} \big(\bigcup_{i \in I} \mu_0(i)\big)$
is defined by the rule
inverse rule, then it is immediate to show that $g{'}$ is a function. To show that $h{'}$ is a function,
we suppose that
$x =_X x{'}$, hence $f(x) =_Y f(x{'})$, and by the definition of $f^{-1} \big(\bigcup_{i \in I} \mu_0(i)\big)$
we get
$e_{\mathsmaller{\bigcup}}^{M(Y)}(i,y) =_Y e_{\mathsmaller{\bigcup}}^{M(Y)}(i{'},y{'})
:\TOT \C E_i^Y(y) =_Y \C E_{i{'}}(y{'})$, hence
$\big(x, (i,y)\big) =_{\mathsmaller{f^{-1} \big(\bigcup_{i \in I} \mu_0(i)\big)}}
\big(x{'}, (i{'},y{'})\big)$. It is immediate to show the commutativity of the
above right diagrams.

Extension theorem for coverings

Let $X, Y$ be sets, and let $\Lambda(X) :=  (\lambda_0, \C E^X, \lambda_1) \in \Fam(I, X)$ be a covering of
$X$. If $f_i \colon \lambda_0(i) \to Y$, for every $i \in I$, such that

\[ {f_i}_{|\lambda_0(i) \cap \lambda_0(j)} =_{\mathsmaller{\D F(\lambda_0(i) \cap \lambda_0(j), Y)}}
{f_j}_{|\lambda_0(i) \cap \lambda_0(j)}, \]

for every $i, j \in I$, there is a unique

$\fXY$ such that $f_{|\lambda_0(i)}
=_{\mathsmaller{\D F(\lambda_0(i), Y)}} f_i$, for every $i \in I$.

Let $e \colon X \eto \bigcup_{i \in I} \lambda_0(i)$ such that the following diagram commutes

(E) at (0,0) $X$;
[right=of E] (B) ;
[right=of B] (F) $\bigcup_{i \in I} \lambda_0(i)$;
[below=of B] (C) ;
[below=of C] (A) $X$.;

[left hook->,bend left] (E) to node [midway,above] $e$ (F);

[right hook->] (E)–(A) node [midway,left] $\id_X \ $;
[left hook->] (F)–(A) node [midway,right] $ \ e_{\mathsmaller{\bigcup}}^{\Lambda(X)}$;

Let the operation
$f \colon X \sto Y$ defined by

\[ f(x) := f_{\pr_1^{\Lambda(X)}(e(x))}\big(\pr_2^{\Lambda(X)}(e(x)\big), \]

for every $x \in X$. Hence, if $x \in X$, and $e(x) := (i, u)$, for some $i \in I$ and $u \in \lambda_0(i)$, then
$f(x) := f_i(u)$. We show that $f$ is a function. Recall that
$ \lambda_0(i) \cap \lambda_0(j) := \big\{(u,w) \in \lambda_0(i) \times \lambda_0(j) \mid \C E_i^X(u)
=_X \C E_j^X(w)\big\}$.
If $x, x{'} \in X$, let $e(x) := (i, u)$ and $e(x{'}) := (j, w)$. If $x =_X x{'}$, then

\[ e(x) =_{\mathsmaller{\bigcup_{i \in I} \lambda_0(i)}} e(x{'}) :\TOT
(i,u) =_{\mathsmaller{\bigcup_{i \in I} \lambda_0(i)}} (j, w) :\TOT \C E_i^X(u) =_X \C E_j^X(w) :\TOT
(u,w) \in \lambda_0(i) \cap \lambda_0(j). \]

By the definition of $f$ we have that $f(x) := f_i(u)$ and $f(x{'}) := f_j(w)$. We show that $f_i(u) =_Y f_j(w)$.
Since $\lambda_0(i) \cap \lambda_0(j)
\subseteq \lambda_0(i)$ and $\lambda_0(i) \cap \lambda_0(j) \subseteq \lambda_0(j)$, and as we have explained right before
Proposition <ref>, by Definition <ref> we have that

\[ {f_i}_{|\lambda_0(i) \cap \lambda_0(j)} := f_i \circ \pr_{\lambda_0(i)} \ \ \& \ \
{f_j}_{|\lambda_0(i) \cap \lambda_0(j)} := f_j \circ \pr_{\lambda_0(j)}. \]

Since $(u,w) \in \lambda_0(i) \cap \lambda_0(j)$,
by the equality of the restrictions of  $f_i$ and $f_j$ to $\lambda_0(i) \cap \lambda_0(j)$

\[ f_i(u) := \big(f_i \circ \pr_{\lambda_0(i)}\big)(u,w) =_Y \big(f_j \circ \pr_{\lambda_0(j)}\big)(u,w) :=
f_j(w). \]

Next we show that, if $i \in I$, then $f_{|\lambda_0(i)} = f_i$. Since $\C E_i^X \colon (\lambda_0(i), \C E_i^X) \subseteq
(X, \id_X)$

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

[left hook->,bend left] (E) to node [midway,above] $\C E_i^X$ (F);

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

by Definition <ref> we have that $f_{|\lambda_0(i)} := f \circ \C E_i^X$. If $u \in \lambda_0(i)$, let
$e\big(\C E_i^X(u)\big) := (j, w)$, for some $j \in I$ and $w \in \lambda_0(j)$. Hence, by the definition of $f$ we get

\[ f_{|\lambda_0(i)}(u) := f\big(\C E_i^X(u)\big) := f_j(w). \]

By the commutativity of the first diagram in this proof we get for $\C E_i^X(u) \in X$

\[ \C E_j^X(w) := e_{\mathsmaller{\bigcup}}^{\Lambda(X)}\big(e\big(\C E_i^X(u)\big)\big) =_X \id_X\big(\C E_i^X(u)\big)
:= \C E_i^X(u) \]

i.e., $(u,w) \in \lambda_0(i) \cap \lambda_0(j)$. Hence, $f_{|\lambda_0(i)}(u) := f_j(w) =_Y f_i(u)$. Finally, let
$f^* \colon X \to Y$ such that $f_{|\lambda_0(i)}^* := f^* \circ \C E_i^X  =_{\mathsmaller{\D F(\lambda_0(i), Y)}} f_i$,
for every $i \in I$. If $x \in X$ let $e(x) := (i, u)$, for some $i \in I$ and $u \in \lambda_0(i)$.
By the commutativity of the first diagram, and since $f^*$ is a function, we get

\begin{align*}
f^*(x) & =_Y f^*\big(e_{\mathsmaller{\bigcup}}^{\Lambda(X)}(e(x))\big)\\
& := f^*\big(e_{\mathsmaller{\bigcup}}^{\Lambda(X)}(i,u)\big)\\
& := f^*\big(\C E_i^X(u)\big)\\
& =_Y f_i(u)\\
& := f_{\pr_1^{\Lambda(X)}(e(x))}\big(\pr_2^{\Lambda(X)}(e(x)\big)\\
& := f(x).\qedhere
\end{align*}

$\Lambda(X) :=  (\lambda_0, \C E^X, \lambda_1) \in \Fam(I, X)$ be a partition of
$X$. If $f_i \colon \lambda_0(i) \to Y$, for every $i \in I$, there is a unique
$\fXY$ with $f_{|\lambda_0(i)}
=_{\mathsmaller{\D F(\lambda_0(i), Y)}} f_i$, for every $i \in I$.

The condition ${f_i}_{|\lambda_0(i) \cap \lambda_0(j)} =_{\mathsmaller{\D F(\lambda_0(i) \cap \lambda_0(j), Y)}}
{f_j}_{|\lambda_0(i) \cap \lambda_0(j)}$ of Theorem <ref> is trivially satisfied using
the logical principle Ex falso quodlibetEx falso quodlibet. If we suppose that $(u,w) \in
\lambda_0(i) \cap \lambda_0(j)$, which is impossible as $\lambda_0(i) \Disj \lambda_0(j)$, the equality
$(f_i \circ \pr_{\lambda_0(i)})(u, w) =_Y (f_j \circ \pr_{\lambda_0(j)})(u, w)$, where $i, j \in I$, follows immediately.

Let $\Lambda(X) := (\lambda_0, \C E^X, \lambda_1)$, $M(X) := (\mu_0, \C Z^X, \mu_1) \in \Fam(I, X)$,
$\Psi : \Lambda(X) \To M(X)$, and $(B, i_B^X) \subseteq X$.

For every $i \in I$ the operation
$e_i^{\Lambda(X)} : \lambda_0(i) \sto \bigcup_{i \in I}\lambda_0(i)$, defined by
$x \mapsto (i, x)$, is an embedding, and $e_i^{\Lambda(X)} \colon \lambda_0(i) \subseteq
\bigcup_{i \in I}\lambda_0(i)$.

If $\lambda_0(i) \subseteq B$, for every $i \in I$, then $\bigcup_{i \in I}\lambda_0(i) \subseteq B$.

The operation
$\bigcup \Psi : \bigcup_{i \in I}\lambda_0(i) \sto \bigcup_{i \in I}\mu_0(i)$, defined by
$\bigcup \Psi (i, x) := (i, \Psi_i (x))$,
is an embedding,

such that for every $i \in I$ the following diagram commutes

(E) at (0,0) $\bigcup_{i \in I}\lambda_0(i)$;
[right=of E] (F) $\bigcup_{i \in I}\mu_0(i)$.;
[above=of F] (A) $\mu_0(i)$;
[above=of E] (D) $\lambda_0(i)$;

[right hook->] (E)–(F) node [midway,below]$\bigcup \Psi$;
[right hook->] (D)–(A) node [midway,above] $\Psi_{i}$;
[right hook->] (D)–(E) node [midway,left] $e_i^{\Lambda(X)}$;
[left hook->] (A)–(F) node [midway,right] $e_i^{M(X)}$;

(i) If $x, x{'} \in \lambda_0(i)$, and since $\C E_i^X$ is an embedding, we have that

\[ e_i^{\Lambda(X)}(x) =_{\mathsmaller{\bigcup_{i \in I}\lambda_0(i)}} e_i^{\Lambda(X)}(x{'}) :\TOT
(i, x) =_{\mathsmaller{\bigcup_{i \in I}\lambda_0(i)}} (i, x{'})
:\TOT \C E_i^X(x) = \C E_i^X(x{'})
\TOT x =_{\lambda_0(i)} x{'}.
\]

Moreover, $e_{\mathsmaller{\bigcup}}^X\big(e_i^{\Lambda(X)}(x)\big) := e_{\mathsmaller{\bigcup}}^X(i, x)
:= \C E_i^X(x)$, hence $e_i^{\Lambda(X)} \colon \lambda_0(i) \subseteq \bigcup_{i \in I}\lambda_0(i)$.

(ii)  If $i \in I$ and $e_i^B \colon \lambda_0(i) \subseteq B$, then $i_B^X(e_i^B(x)) =_X \C E^X_i(x)$,
for every $x \in \lambda_0(i)$. Let the operation $e^B \colon \bigcup_{i \in I}\lambda_0(i) \sto B$,
defined by $e^B(i,x) :=
e_i^B(x)$, for every $(i,x)  \in \bigcup_{i \in I}\lambda_0(i)$. The operation $e^B$ is a function:

\begin{align*}
(i, x) =_{\mathsmaller{\bigcup_{i \in I}\lambda_0(i)}} (j, y) & :\TOT \C E_i^X(x) =_X \C E_j^X(y)\\
& \To i_B^X(e_i^B(x)) =_X i_B^X(e_j^B(y))\\
& \To e_i^B(x) =_X e_j^B(y)\\
& :\TOT e^B(i,x) =_X e^B(j,y).
\end{align*}

Moroever, $i_B^X\big(e^B(i,x)\big) := i_B^X(e_i^B(x)) =_X \C E_i^X(x) := e_{\mathsmaller{\bigcup}}^{\Lambda(X)}(i,x)$,
hence $e^B \colon \bigcup_{i \in I}\lambda_0(i) \subseteq B$.

(iii) The required commutativity of the diagram is immediate, and $\bigcup \Psi$ is an embedding, since

(E) at (0,0) ;
[right=of E] (F) $X$;
[above=of E] (A) $\lambda_0 (i)$;
[right=of F] (B) ;
[above=of B] (G) $\mu_0 (i)$;
[right=of G] (C) $\lambda_0 (j)$;
[right=of C] (D) ;
[right=of D] (E) $\mu_0 (j)$;
[below=of D] (H) $X$,;

[right hook->] (A)–(F) node [midway,left] $\C E_{i}^X \ $;
[left hook->] (G)–(F) node [midway,right] $\ \C Z_i^X$;
[right hook->] (A)–(G) node [midway,above] $\Psi_{i}$;
[right hook->] (C)–(H) node [midway,left] $\C E_{j}^X \ $;
[left hook->] (E)–(H) node [midway,right] $\ \C Z_j^X$;
[right hook->] (C)–(E) node [midway,above] $\Psi_{j}$;

\begin{align*}
(i, x) =_{\mathsmaller{\bigcup_{i \in I} \lambda_0(i)}} (j, y) & :\Leftrightarrow \C E_i^X (x) =_X \C E_j^X (y)\\
& \TOT \C Z_i^X(\Psi_i(x)) =_X \C Z^X_j(\Psi_j(y))\\
& :\TOT (i, \Psi_i(x)) =_{\mathsmaller{\bigcup_{i \in I} \mu_0(i)}} (j, \Psi_j(y))\\
& :\TOT \bigcup \Psi (i, x) =_{\mathsmaller{\bigcup_{i \in I} \mu_0(i)}} \bigcup \Psi (j, y).\qedhere
\end{align*}

§ THE INTERSECTION OF A FAMILY OF SUBSETS

Let $\Lambda(X) := (\lambda_0, \C E^X, \lambda_1) \in \Fam(I, X)$, and $i_0 \in I$.
The intersection $\bigcap_{i \in I} \lambda_0 (i)$intersection of a family of
subsets$\bigcap_{i \in I} \lambda_0 (i)$ of $\Lambda(X)$ is the
totality defined by

\[ \Phi \in \bigcap_{i \in I} \lambda_0 (i) : \TOT \Phi \in \D A(I, \lambda_0)
% : \bigcurlywedge_{i \in I}\lambda_0 (i)
\ \& \ \forall_{i, j \in I}\big(\C E_i^X (\Phi_i) =_X \C E_{j}^X (\Phi_{j})\big). \]

Let $e_{\mathsmaller{\bigcap}}^{\Lambda(X)} : \bigcap_{i \in I} \lambda_0 (i) \sto X$ be defined by
$e_{\mathsmaller{\bigcap}}^{\Lambda(X)}(\Phi) := \C E_{i_0}^X\big(\Phi_{i_0}\big)$, for
every $\Phi \in \bigcap_{i \in I} \lambda_0 (i)$, and

\[ \Phi =_{\mathsmaller{\bigcap_{i \in I} \lambda_0 (i)}} \Theta : \TOT e_{\mathsmaller{\bigcap}}^{\Lambda(X)}(\Phi)
=_X e_{\mathsmaller{\bigcap}}^{\Lambda(X)}(\Theta) :\TOT
\C E_{i_0}^X\big(\Phi_{i_0}\big) =_X \C E_{i_0}^X\big(\Theta_{i_0}\big),
\]

If $\neq_X$ is a given inequality on $X$, let
$\Phi \neq_{\mathsmaller{\bigcap_{i \in I} \lambda_0 (i)}} \Theta :\TOT
\C E_{i_0}^X\big(\Phi_{i_0}\big) \neq_X \C E_{i_0}^X\big(\Theta_{i_0}\big)$.

Clearly, $=_{\bigcap_{i \in I} \lambda_0(i)}$ is an equality on
$\bigcap_{i \in I} \lambda_0(i)$, which is considered to be a set, and $e_{\mathsmaller{\bigcap}}^{\Lambda(X)}$
is an embedding, hence $\big(\bigcap_{i \in I} \lambda_0(i),
e_{\mathsmaller{\bigcap}}^{\Lambda(X)}\big) \subseteq X$. Moreover, the inequality
$\neq_{\mathsmaller{\bigcap_{i \in I} \lambda_0(i)}}$ is the canonical inequality of the subset
$\bigcap_{i \in I} \lambda_0(i)$ of $X$ (see Corollary <ref>).

Let $\Lambda(X) := (\lambda_0, \C E^X, \lambda_1) \in \Fam(I, X)$.

$\Phi =_{\bigcap_{i \in I} \lambda_0 (i)} \Theta \TOT \Phi =_{\D A(I, \lambda_0)} \Theta$.

If $\Phi \in \bigcap_{i \in I} \lambda_0 (i)$, then $\Phi \in \prod_{i \in I}\lambda_0(i)$.

If $(X, =_X, \neq_X)$ is discrete, the set $\big(\bigcap_{i \in I} \lambda_0(i),
=_{\mathsmaller{\bigcap_{i \in I} \lambda_0(i)}}, \neq_{\mathsmaller{\bigcap_{i \in I} \lambda_0(i)}}\big)$ is discrete.

(i) To show the implication $(\To)$, if $i \in I$, then
$\C E_i^X(\Phi_i) =_X \C E_{i_0}^X (\Phi_{i_0}) =_X \C E_{i_0}^X (\Theta_{i_0}) =_X \C E_i^X(\Theta_i),$
and since $\C E_i^X$ is an embedding, $\Phi_i =_{\lambda_0(i)} \Theta_i$. For the converse implication,
the pointwise equality of $\Phi$ and $\Theta$ implies that $\Phi_{i_0} =_{\lambda_0(i_0)} \Theta_{i_0}$, hence
$\C E_{i_0}^X (\Phi_{i_0}) =_X \C E_{i_0}^X (\Theta_{i_0})$.

(ii) If $i =_I j$, then
$\C E_j^X \big(\lambda_{ij}(\Phi_i)\big) =_X \C E_i^X(\Phi_i) =_X \C E_j(\Phi_j)$,
and as $\C E_j^X$ is an embedding, we get the required equality $\lambda_{ij}(\Phi_i) =_{\lambda_0(j)}
\Phi_j$. The proof of (iii) is immediate.

Since the equality of $\prod_{i \in I}\lambda_0(i)$ is the pointwise equality of $\D A(I, \lambda_0)$,
then, as we explained above, the equality of $\prod_{i \in I}\lambda_0(i)$ is the equality of
$\bigcap_{i \in I} \lambda_0 (i)$.

Let $i_0 \in I$, $(A, i_A^X) \subseteq X$, and $C^A(X) := (\lambda_0^A, \C E^{A, X}, \lambda_1^A) \in \Fam(I, X)$
the constant family $A$ of subsets of $X$. Then

\[ \bigcap_{i \in I}A := \bigcap_{i \in I}\lambda_0^A(i) =_{\C P(X)} A. \]

We proceed similarly to the proof of Remark <ref>.

If $\Lambda^{\D 2}(X)$ is the $\D 2$-family of subsets $A, B$ of $X$,

$\bigcap_{i \in \D 2} \lambda_0^{\D 2}(i) =_{\C P(X)} A \cap B.$

By definition $\Phi \in \bigcap_{i \in I} \lambda_0^{\D 2} (i) : \TOT \Phi \colon \bigcurlywedge_{i \in I}\lambda_0^{\D 2}
(i)$ and for every $i, j \in \D 2$ we have that $\C E_i^X (\Phi_i) =_X \C E_{j}^X (\Phi_{j})$,
where $\C E_0^X := i_A^X$ and
$\C E_1^X := i_B^X$. Moreover, $e_{\mathsmaller{\bigcap}}^{\Lambda^{\D 2}(X)} : \bigcap_{i \in I}
\lambda_0^{\D 2} (i) \sto X$ is
given by $e_{\mathsmaller{\bigcap}}^{\Lambda^{\D 2}(X)}(\Phi) := \C E_{0}^X\big(\Phi_{0}\big)$,
for every $\Phi \in \bigcap_{i \in I}
\lambda_0^{\D 2} (i)$, and $\Phi =_{\mathsmaller{\bigcap_{i \in I} \lambda_0^{\D 2} (i)}} \Theta :\TOT
\C E_{0}^X\big(\Phi_{0}\big) =_X \C E_{0}^X\big(\Theta_{0}\big)$. Let $f \colon A \cap B
\sto \bigcap_{i \in \D 2} \lambda_0^{\D 2}(i)$ be defined by $f(a,b) := \Phi_{(a,b)}$, for every $(a,b) \in A \cap B$,
where $\Phi_{(a,b)} \colon \bigcurlywedge_{i \in I}\lambda_0^{\D 2}(i)$, such that
$\Phi_{(a,b)}(0) := a$ and $\Phi_{(a,b)}(1) := b$.

Since $\C E_0^X\big(\Phi_{(a,b)}(0)\big) =_X \C E_1^X\big(\Phi_{(a,b)}(1)\big) \TOT \C E_0^X(a) =_X
\C E_1(b) :\TOT i_A^X(a) =_X i_B^X(b)$, where the last equality holds by the definition of $A \cap B$
(see Definition <ref>), the operation $f$ is well-defined. It is straightforward
to show that $f$ is a
function. Let the operation $g \colon \bigcap_{i \in \D 2} \lambda_0^{\D 2}(i) \sto A \cap B$, defined by
$g(\Phi) := (\Phi_0, \Phi_1)$, for every $\Phi \in \bigcap_{i \in \D 2} \lambda_0^{\D 2}(i)$.
Since $i_Z^X(\Phi_0) := \C E_0^X(\Phi_0) =_X \C E_1^X(\Phi_1) := i_B^X(\Phi_1)$, we have that
$g$ is well-defined. It is easy to show that $g$ is a function,

(E) at (0,0) $A \cap B$;
[right=of E] (B) ;
[right=of B] (F) $\mathsmaller{\bigcap_{i \in \D 2} \lambda_0^{\D 2}(i)}$;
[below=of B] (C) ;
[below=of C] (A) $X$.;

[left hook->,bend left] (E) to node [midway,above] $f$ (F);
[left hook->,bend left] (F) to node [midway,below] $g$ (E);
[right hook->] (E)–(A) node [midway,left] $i_{A \cap B}^X \ $;
[left hook->] (F)–(A) node [midway,right] $ \ e_{\mathsmaller{\bigcap}}^{\Lambda^{\D 2}(X)}$;

and the above inner diagrams commute.

Let $\Lambda(X) := (\lambda_0, \C E^X, \lambda_1) \in \Fam(I, X)$ and $M(Y) := (\mu_0, \C E^Y, \mu_1) \in \Fam(I, Y)$.
If $\fXY$, the following hold:

$f \bigg(\bigcap_{i \in I} \lambda_0(i)\bigg) \subseteq \bigcap_{i \in I} f\big(\lambda_0(i)\big)$.

$f^{-1} \bigg(\bigcap_{i \in I} \mu_0(i)\bigg) =_{\C P(X)} \bigcap_{i \in I} f^{-1}\big(\mu_0(i)\big)$.

We proceed similarly to the proof of Proposition <ref>.

Let $\Lambda(X) := (\lambda_0, \C E^X, \lambda_1), M_X := (\mu_0, \C Z^X, \mu_1) \in \Fam(I,X)$, let $i_0 \in I$,
$\Psi : \Lambda(X) \To M(X)$, and $(B, i_B^X) \subseteq X$.

The operation
$\pi_i^{\Lambda(X)} : \bigcap_{i \in I}\lambda_0(i) \sto \lambda_0(i)$, defined by
$\Theta \mapsto \Theta_i,$ is a function, and $\pi_i^{\Lambda(X)} \colon \bigcap_{i \in I}\lambda_0(i)
\subseteq \lambda_0(i)$, for every $i \in I$.

If $B \subseteq \lambda_0(i)$, for every $i \in I$, then $B \subseteq \bigcap_{i \in I}\lambda_0(i)$.

The operation
$\bigcap \Psi : \bigcap_{i \in I}\lambda_0(i) \sto \bigcap_{i \in I}\mu_0(i)$, defined by
$[\bigcap \Psi (\Theta)]_i := \Psi_i (\Theta_i)$, for every $i \in I$, is an embedding,

such that for every $i \in I$
the following diagram commutes

(E) at (0,0) $\bigcap_{i \in I}\lambda_0(i)$;
[right=of E] (F) $\bigcap_{i \in I}\mu_0(i)$.;
[above=of F] (A) $\mu_0(i)$;
[above=of E] (D) $\lambda_0(i)$;

[right hook->] (E)–(F) node [midway,below]$\bigcap \Psi$;
[right hook->] (D)–(A) node [midway,above] $\Psi_{i}$;
[->] (E)–(D) node [midway,left] $\pi_i^{\Lambda(X)}$;
[->] (F)–(A) node [midway,right] $\pi_i^{M(X)}$;

(i) Since $\Phi =_{\bigcap_{i \in I} \lambda_0 (i)} \Theta \To \Phi =_{\D A(I, \lambda_0)} \Theta$, we get
$\Phi_i = \Theta_i$, for every $i \in I$. Since $\C E_i^X\big(\pi_i^{\Lambda(X)}(\Theta)\big) := \C E_i^X(\Theta_i) =_X
\C E_{i_0}^X(\Theta_{i_0}) := e^X_{\mathsmaller{\bigcap}}(\Theta)$, we get
$\pi_i^{\Lambda(X)} \colon \bigcap_{i \in I}\lambda_0(i) \subseteq \lambda_0(i)$.

(ii) If $i \in I$, let $e_B^i \colon B \subseteq \lambda_0(i)$, hence $\C E_i^X(e_B^i(b)) =_X i_B^X(b)$,
for every $b \in B$.
Let the operation $e_B \colon B \sto \bigcap_{i \in I}\lambda_0(i)$, defined by the rule $b \mapsto e_B(b)$,
$[e_B(b)]_i := e_B^i(b)$, for every $b \in B$ and $i \in I$. First we show that $e_B$ is well defined.
If $i, j \in I$, then

\[\C E_i^X\big([e_B(b)]_i\big) =_X \C E_j^X\big([e_B(b)]_j\big) :\TOT \C E_i^X(e_B^i(b)) =_X \C E_j^X(e_B^j(b)) \TOT
i_B^X(b) =_X i_B^X(b). \]

Clearly, $e_B$ is a function. Moreover, $e_B \colon B \subseteq \bigcap_{i \in I}\lambda_0(i)$, since,
for every $b \in B$,

\[ e_{\mathsmaller{\bigcap}}(e_B(b)) := \C E_{i_0}^X\big([e_B(b)]_{i_0}\big) :=
\C E_{i_0}^X(e_B^{i_0}(b)) =_X i_B^X(b). \]

(iii) It suffices to show that $\bigcap \Psi$ is an embedding.
If $\Phi, \Theta \in \bigcap_{i \in I} \lambda_0 (i)$, then

\begin{align*}
\Phi =_{\mathsmaller{\bigcap_{i \in I} \lambda_0 (i)}} \Theta & :\TOT
\C E_{i_0}^X\big(\Phi_{i_0}\big) =_X \C E_{i_0}^X\big(\Theta_{i_0}\big) \\
& \TOT \C Z_{i_0}^X(\Psi_{i_0}(\Phi_{i_0})) =_X \C Z^X_{i_0}(\Psi_{i_0}(\Theta_{i_0}))\\
& :\TOT \C Z_{i_0}^X\bigg(\bigg[\bigcap \Psi(\Phi)\bigg]_{i_0}\bigg) =_X
\C Z_{i_0}^X\bigg(\bigg[\bigcap \Psi(\Theta)\bigg]_{i_0}\bigg)\\
& :\TOT \bigg(\bigcap \Psi\bigg) (\Phi) =_{\mathsmaller{\bigcap_{i \in I} \mu_0 (i)}}
\bigg(\bigcap \Psi\bigg)(\Theta).\qedhere
\end{align*}

The above notions and results can be generalised as follows.

Let $X$ and $Y$ be sets, and $h : X \to Y$.
If $\Lambda(X) := (\lambda_0, \C E^X, \lambda_1) \in \Fam(I,X)$, and
$M(Y) := (\mu_0, \C Z^Y, \mu_1) \in \Fam(I,Y)$, a
family of subsets-map from $\Lambda(X)$ to $M(Y)$ is a dependent operation
$\Psi : \bigcurlywedge_{i \in I}\D F\big(\lambda_0(i), \mu_0(i)\big)$, where if
$\Psi(i) := \Psi_i$, for every $i \in I$, then, for every $i \in I$, the following diagram commutes

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

[right hook->] (E)–(A) node [midway,left] $\C E_{i}^X \ $;
[left hook->] (F)–(B) node [midway,right] $\ \C Z^Y_i$;
[->] (E)–(F) node [midway,above] $\Psi_{i}$;
[->] (A)–(B) node [midway,below] $h$;

The totality $\Map_{I,h}(\Lambda(X), M(Y))$$\Map_{I,h}(\Lambda(X), M(Y))$ of family of
subsets-maps from $\Lambda(X)$ to $M(Y)$ is
equipped with the pointwise equality,

and we write $\Psi \colon \Lambda(X) \stackrel{h \ } \To M(Y)$$\Psi \colon \Lambda(X) \stackrel{h \ } \To M(Y)$,
if $\Psi \in \Map(\Lambda(X), M(X))$.

$\Xi \colon M(Y) \stackrel{g \ } \To N(Z)$, where $g
\colon Y \to Z$, the composition family of subsets-map
$\Xi \circ \Psi : \Lambda(X) \stackrel{g \circ h} \Longrightarrow N(Z)$ is defined by
$(\Xi \circ \Psi)(i) := \Xi_i \circ \Psi_i$, for every $i \in I$

(E) at (0,0) $\lambda_0(i)$;
[right=of E] (F) $\mu_0(i)$;
[right=of F] (G) $\nu_0(i)$;
[below=of E] (A) $X$;
[below=of F] (B) $Y$;
[below=of G] (C) $Z$.;

[right hook->] (E)–(A) node [midway,left] $\C E_{i}^X \ $;
[left hook->] (F)–(B) node [midway,right] $\ \C Z_i^Y$;
[left hook->] (G)–(C) node [midway,right] $\C H_i^Z$;
[->] (E)–(F) node [midway,above] $\Psi_{i}$;
[->] (A)–(B) node [midway,below] $h$;
[->] (F)–(G) node [midway,above] $\Xi_i$;
[->] (B)–(C) node [midway,below] $g$;

If $Y := X$, and $h := \id_X$, and if $\Psi \colon \Lambda(X) \stackrel{\id_X} \Longrightarrow
M(X)$, then $\Psi \colon \Lambda(X) \To M(X)$. In the general case, if
$\Psi \colon \Lambda(X) \stackrel{h \ } \To M(Y)$, then $\Psi_i$ is an embedding, if $h$ is an embedding.

Let $X$ and $Y$ be sets, and $h : X \to Y$. Let also $\Lambda(X) := (\lambda_0, \C E^X, \lambda_1) \in \Fam(I,X)$,
$M(Y) := (\mu_0, \C Z^Y, \mu_1) \in \Fam(I,Y)$, and $\Psi \colon \Lambda(X) \stackrel{h \ } \To M(Y)$.

The operation
$\bigcup_h \Psi : \bigcup_{i \in I}\lambda_0(i) \sto \bigcup_{i \in I}\mu_0(i)$, defined by
$\big(\bigcup_h \Psi\big) (i, u) := (i, \Psi_i (u))$, for every $(i, u) \in \bigcup_{i \in I}\lambda_0(i)$, is
a  function,

and for every $i \in I$ the following left diagram commutes

(E) at (0,0) $\bigcup_{i \in I}\lambda_0(i)$;
[right=of E] (F) $\bigcup_{i \in I}\mu_0(i)$;
[above=of F] (A) $\mu_0(i)$;
[above=of E] (D) $\lambda_0(i)$;

[right=of F] (G) $\bigcap_{i \in I}\lambda_0(i)$;
[right=of G] (K) $\bigcap_{i \in I}\mu_0(i)$.;
[above=of K] (L) $\mu_0(i)$;
[above=of G] (M) $\lambda_0(i)$;

[->] (E)–(F) node [midway,below]$\bigcup_h \Psi$;
[->] (D)–(A) node [midway,above] $\Psi_{i}$;
[right hook->] (D)–(E) node [midway,left] $e_i^{\Lambda(X)}$;
[left hook->] (A)–(F) node [midway,right] $e_i^{M(Y)}$;

[->] (G)–(K) node [midway,below]$\bigcap_h \Psi$;
[->] (M)–(L) node [midway,above] $\Psi_{i}$;
[->] (G)–(M) node [midway,left] $\pi_i^{\Lambda(X)}$;
[->] (K)–(L) node [midway,right] $\pi_i^{M(Y)}$;

If $i_0 \in I$, the operation
$\bigcap_h \Psi : \bigcap_{i \in I}\lambda_0(i) \sto \bigcap_{i \in I}\mu_0(i)$, defined by
$[\bigcap_h \Psi (\Theta)]_i := \Psi_i (\Theta_i)$, for every $i \in I$, is a function,

such that for every $i \in I$ the above right diagram commutes.

(i) The commutativity of the diagram is trivial, and we show that $\bigcup_h \Psi$ is a function:

\begin{align*}
(i, u) =_{\mathsmaller{ \bigcup_{i \in I}\lambda_0(i)}} (j, w) & :\TOT \C E_i(u) =_X \C E_j(w)\\
& \To h(\C E_i(u)) =_Y h(\C E_j(w))\\
& \TOT E_i(\Psi_i(u)) =_Y E_j(\Psi_j(w))\\
& :\TOT (i, \Psi_i(u)) =_{\mathsmaller{\bigcup_{i \in I}\mu_0(i)}} (j, \Psi_j(w))\\
& :\TOT \bigg(\bigcup_h \Psi\bigg) (i, u) =_{\mathsmaller{\bigcup_{i \in I}\mu_0(i)}} \bigg(\bigcup_h \Psi\bigg)
(j, w).
\end{align*}

(ii) The commutativity of the diagram is trivial, and we show that $\bigcap_h \Psi$ is a function:

\begin{align*}
\Phi =_{\mathsmaller{\bigcap_{i \in I}\lambda_0(i)}} \Theta & \TOT \C E_{i_0}(\Phi_{i_0}) =_X
\C E_{i_0}(\Theta_{i_0})\\
& \To h\big(\C E_{i_0}(\Phi_{i_0})\big) =_Y h \big(\C E_{i_0}(\Theta_{i_0})\big)\\
& \TOT E_{i_0}\big(\Psi_{i_0}(\Phi_{i_0})\big) =_Y E_{i_0}\big(\Psi_{i_0}(\Theta_{i_0})\big)\\
& :\TOT E_{i_0}\bigg(\bigg[\bigcap_h \Psi (\Phi)\bigg]_{i_0}\bigg) =_Y
E_{i_0}\bigg(\bigg[\bigcap_h \Psi (\Theta)\bigg]_{i_0}\bigg)\\
& :\TOT \bigg(\bigcap_h \Psi\bigg) (\Phi) =_{\mathsmaller{\bigcap_{i \in I}\mu_0(i)}}
\bigg(\bigcap_h \Psi\bigg) (\Theta).\qedhere
\end{align*}

§ FAMILIES OF SUBSETS OVER PRODUCTS

Let $\Lambda(X) := (\lambda_0, \C E^X, \lambda_1), K(X) := (k_0, \C H^X, k_1) \in \Fam(I, X)$,
$M(Y) := (\mu_0, \C E^Y, \mu_1)$, and $N(Y) := (\nu_0, \C H^Y, \nu_1) \in \Fam(J, Y)$.

$(\Lambda \otimes M)(X \times Y) := (\lambda_0 \otimes \mu_0, \C E^X \otimes \C E^Y, \lambda_1 \otimes \mu_1)
\in \Fam(I \times J, X
\times Y)$, where

\[ (\lambda_0 \otimes \mu_0)(i,j) := \lambda_0(i) \times \mu_0(j); \ \ \ \ (i,j) \in I \times J, \]

\[ \big(\C E^X \otimes \C E^Y\big)_{(i,j)} \colon \lambda_0(i) \times \mu_0(j) \eto X \times Y, \]

\[  \big(\C E^X \otimes \C E^Y\big)_{(i,j)}(u, w) := \big(\C E^X_i(u), \C E^Y_j(w)\big); \ \ \ \
(u,w) \in \lambda_0(i) \times \mu_0(j), \ (i,j) \in I \times J,
\]

\[  (\lambda_1 \otimes \mu_1)_{(i,j)(i{'}j{'})} \colon \lambda_0(i) \times \mu_0(j) \to \lambda_0(i{'})
\times \mu_0(j{'}),  \]

\[ (\lambda_1 \otimes \mu_1)_{(i,j)(i{'}j{'})}(u, w) := \big(\lambda_{ii{'}}(u), \mu_{jj{'}}(w)\big); \ \ \ \
(u,w) \in \lambda_0(i) \times \mu_0(j).
\]

If $\Phi \colon \Lambda(X) \To K(X)$ and $\Psi \colon M(X) \To N(X)$, then $\Phi \otimes \Psi \colon
(\Lambda \otimes M)(X \times Y) \To (K \otimes N)(X \times Y)$, where, for every $(i,j) \in I \times J$,

\[ (\Phi \otimes \Psi)_{(i,j)} \colon \lambda_0(i) \times \mu_0(j) \to k_0(i) \times \nu_0(j),  \]

\[  (\Phi \otimes \Psi)_{(i,j)}(u,w) := \big(\Phi_i(u), \Psi_j(w)\big); \ \ \ \ (u,w) \in \lambda_0(i) \times \mu_0(j).
\]

The following equality holds

\[ \bigcup_{(i,j) \in I \times J}\big(\lambda_0(i) \times \mu_0(j)\big)
=_{\C P(X \times Y)} \bigg(\bigcup_{i \in I}\lambda_0(i)\bigg)
\times \bigg(\bigcup_{j \in J}\mu_0(j)\bigg). \]

If $i_0 \in I$ and $j_0 \in J$, the following equality holds

\[ \bigcap_{(i,j) \in I \times J}\big(\lambda_0(i) \times \mu_0(j)\big) =_{\C P(X \times Y)}
\bigg(\bigcap_{i \in I}\lambda_0(i)\bigg)
\times \bigg(\bigcap_{j \in J}\mu_0(j)\bigg). \]

If $\Lambda(X)$ covers $X$ and $M(Y)$ covers $Y$, then $(\Lambda \otimes M)(X \times Y)$
covers $X \times Y$.

Let the inequalities $\neq_I, \neq_J, \neq_X$ and $\neq_Y$ on $I, J, X$ and $Y$, respectively.
If $\Lambda(X)$ is a partition of $X$ and $M(Y)$ is a partition of $Y$, then $(\Lambda \otimes M)(X \times Y)$
is a partition of $X \times Y$.

The proofs of (i)-(iv) are the internal analogue to the proofs of Proposition <ref>(i)-(iii).

(v) Since $X =_{\C P(X)} \bigcup_{i \in I} \lambda_0(i)$ and $Y =_{\C P(Y)} \bigcup_{j \in J} \mu_0(j)$, by case
(iii) and by Proposition <ref>(iv) we have that

\[ X \times Y =_{\C P(X \times Y)} \bigg(\bigcup_{i \in I}\lambda_0(i)\bigg)
\times \bigg(\bigcup_{j \in J}\mu_0(j)\bigg) =_{\C P(X \times Y)}
\bigcup_{(i,j) \in I \times J}\big(\lambda_0(i) \times \mu_0(j)\big).
\]

(vi) By Definition <ref> we have that

\[ i \neq_I i{'} \To \C E_i^X(u) \neq_X \C E_{i{'}}^X (u{'}); \ \ \ \ i, i{'} \in I, \ u \in \lambda_0(i), \ u{'} \in
\lambda_0(i{'}),
\]

\[ j \neq_J j{'} \To \C E_i^Y(w) \neq_Y \C E_{j{'}}^Y (w{'}); \ \ \ \ j, j{'} \in J, \ w \in \mu_0(j), \ w{'} \in
\mu_0(j{'}).
\]

Let $(i,j) \neq_{I \times J} (i{'}, j{'}) :\TOT i \neq_I i{'} \vee j \neq_J j{'}$. If $i \neq_I i{'}$ is the case, then
$\C E_i^X(u) \neq_X \C E_{i{'}}^X (u{'})$, hence $ \big(\C E^X_i(u), \C E^Y_j(w)\big) \neq_{X \times Y}
\big(\C E^X_i(u{'}), \C E^Y_j(w{'})\big)$. If $j \neq_J j{'}$, we proceed similarly.

Let $\Lambda(X) := (\lambda_0, \C E^X, \lambda_1), K(X) := (k_0, \C H^X, k_1) \in \Fam(I, X)$,
$M(X) := (\mu_0, \C Z^X, \mu_1)$, and $N(X) := (\nu_0, \C F^X, \nu_1) \in \Fam(J, X)$.

$(\Lambda \wedge M)(X) := (\lambda_0 \wedge \mu_0, \C E^X \wedge \C Z^X, \lambda_1 \wedge \mu_1)
\in \Fam(I \times J, X)$, where

\[ (\lambda_0 \wedge \mu_0)(i,j) := \lambda_0(i) \cap \mu_0(j); \ \ \ \ (i,j) \in I \times J, \]

\[ \big(\C E^X \wedge \C Z^X\big)_{(i,j)} \colon \lambda_0(i) \cap \mu_0(j) \eto X, \]

\[  \big(\C E^X \wedge \C Z^X\big)_{(i,j)}(u, w) := \C E^X_i(u); \ \ \ \
(u,w) \in \lambda_0(i) \cap \mu_0(j), \ (i,j) \in I \times J,
\]

\[  (\lambda_1 \wedge \mu_1)_{(i,j)(i{'}j{'})} \colon \lambda_0(i) \cap \mu_0(j) \to \lambda_0(i{'})
\cap \mu_0(j{'}),  \]

\[ (\lambda_1 \otimes \mu_1)_{(i,j)(i{'}j{'})}(u, w) := \big(\lambda_{ii{'}}(u), \mu_{jj{'}}(w)\big); \ \ \ \
(u,w) \in \lambda_0(i) \cap \mu_0(j).
\]

$(\Lambda \vee M)(X) := (\lambda_0 \vee \mu_0, \C E^X \vee \C Z^X, \lambda_1 \vee \mu_1)
\in \Fam(I \times J, X)$, where

\[ (\lambda_0 \vee \mu_0)(i,j) := \lambda_0(i) \cup \mu_0(j); \ \ \ \ (i,j) \in I \times J, \]

\[ \big(\C E^X \vee \C Z^X\big)_{(i,j)} \colon \lambda_0(i) \cup \mu_0(j) \eto X, \]

\[ \big(\C E^X \vee \C Z^X\big)_{(i,j)}(z) := \left\{ \begin{array}{ll}
\C E_i^X(z)    &\mbox{, $z \in \lambda_0(i)$}\\
\C Z_j^Y(z)             &\mbox{, $z \in \mu_0(j)$}
\end{array}
\right.
; \ \ \ \ i \in I, \ z \in \lambda_0(i) \cup \mu_0(i) \]

\[  (\lambda_1 \vee \mu_1)_{(i,j)(i{'}j{'})}(z) := \left\{ \begin{array}{ll}
\lambda_{ii{'}}(z)    &\mbox{, $z \in \lambda_0(i)$}\\
\mu_{jj{'}}(z)             &\mbox{, $z \in \mu_0(j)$}
\end{array}
\right.
; \ \ \ \ \big((i,j),(i{'}j{'})\big) \in D(I \times J).
\]

If $\Phi \colon \Lambda(X) \To K(X)$ and $\Psi \colon M(X) \To N(X)$, then $\Phi \wedge \Psi \colon
(\Lambda \wedge M)(X) \To (K \wedge N)(X)$, where, for every $(i,j) \in I \times J$,

\[ (\Phi \wedge \Psi)_{(i,j)} \colon \lambda_0(i) \cap \mu_0(j) \to k_0(i) \cap \nu_0(j),  \]

\[  (\Phi \wedge \Psi)_{(i,j)}(u,w) := \big(\Phi_i(u), \Psi_j(w)\big); \ \ \ \ (u,w) \in \lambda_0(i) \cap \mu_0(j).
\]

If $\Phi \colon \Lambda(X) \To K(X)$ and $\Psi \colon M(X) \To N(X)$, then $\Phi \vee \Psi \colon
(\Lambda \vee M)(X) \To (K \vee N)(X)$, where, for every $(i,j) \in I \times J$,

\[ (\Phi \wedge \Psi)_{(i,j)} \colon \lambda_0(i) \cup \mu_0(j) \to k_0(i) \cup \nu_0(j),  \]

\[ (\Phi \vee \Psi)_{(i,j)}(z) := \left\{ \begin{array}{ll}
\Phi_i(z)    &\mbox{, $z \in \lambda_0(i)$}\\
\Psi_j(z)             &\mbox{, $z \in \mu_0(j)$.}
\end{array}
\right.
\]

The following equality holds

\[ \bigcup_{(i,j) \in I \times J}\big(\lambda_0(i) \cap \mu_0(j)\big) =_{\C P(X)} \bigg(\bigcup_{i \in I}\lambda_0(i)\bigg)
\cap \bigg(\bigcup_{j \in J}\mu_0(j)\bigg). \]

If $(i_0, j_0) \in I \times J$, the following equality holds

\[ \bigcap_{(i,j) \in I \times J}\big(\lambda_0(i) \cup \mu_0(j)\big) =_{\C P(X)} \bigg(\bigcap_{i \in I}\lambda_0(i)\bigg)
\cup \bigg(\bigcap_{j \in J}\mu_0(j)\bigg). \]

If $\Lambda(X)$ covers $X$ and $M(Y)$ covers $Y$, then $(\Lambda \wedge M)(X)$
covers $X$.

Let the inequalities $\neq_I, \neq_J, \neq_X$ and $\neq_Y$ on $I, J, X$ and $Y$, respectively.
If $\Lambda(X)$ is a partition of $X$ and $M(Y)$ is a partition of $Y$, then $(\Lambda \wedge M)(X)$
is a partition of $X$.

We proceed as in the proof of Proposition <ref>.

Let $M(Y) := (\mu_0, \C Z^Y, \mu_1) \in \Fam(J, Y)$, $(A, i_A^X) \subseteq X$, $(B, i_B^Y) \subseteq Y$, and let
$\Lambda^A(X) := (\lambda_0^A, \C E^{A,X}, \lambda_1^X) \in \Fam(\D 1, X)$ the constant family $A$ of
subsets of $X$, and $\Lambda^B := (\lambda_0^B, \C E^{B, Y}, \lambda_1^B)$ the constant family $B$ of subsets of $Y$. By
Propositions <ref> and <ref> we have that

\begin{align*}
\bigcup_{j \in J}(A \times \mu_0(j)) & := \bigcup_{(i,j) \in \D 1 \times J}A \times \mu_0(j)\\
& := \bigcup_{(i,j) \in \D 1 \times J}\big(\lambda_0^A(i) \times \mu_0(j)\big)\\
& =_{\C P(X \times Y)} \bigg(\bigcup_{i \in \D 1}\lambda_0^A(i)\bigg) \times \bigg(\bigcup_{j \in J}\mu_0(j)\bigg)\\
& =_{\C P(X \times Y)} A \times \bigg(\bigcup_{j \in J}\mu_0(j)\bigg),
\end{align*}

\begin{align*}
\bigcap_{j \in J}(A \times \mu_0(j)) & := \bigcap_{(i,j) \in \D 1 \times J}A \times \mu_0(j)\\
& := \bigcap_{(i,j) \in \D 1 \times J}\big(\lambda_0^A(i) \times \mu_0(j)\big)\\
& =_{\C P(X \times Y)} \bigg(\bigcap_{i \in \D 1}\lambda_0^A(i)\bigg) \times \bigg(\bigcap_{j \in J}\mu_0(j)\bigg)\\
& =_{\C P(X \times Y)} A \times \bigg(\bigcap_{j \in J}\mu_0(j)\bigg),
\end{align*}

\begin{align*}
\bigcup_{j \in J}(B \cap \mu_0(j)) & := \bigcup_{(i,j) \in \D 1 \times J}B \cap \mu_0(j)\\
& := \bigcup_{(i,j) \in \D 1 \times J}\big(\lambda_0^B(i) \cap \mu_0(j)\big)\\
& =_{\C P(Y)} \bigg(\bigcup_{i \in \D 1}\lambda_0^B(i)\bigg) \cap \bigg(\bigcup_{j \in J}\mu_0(j)\bigg)\\
& =_{\C P(Y)} B \cap \bigg(\bigcup_{j \in J}\mu_0(j)\bigg),
\end{align*}

\begin{align*}
\bigcap_{j \in J}(B \cup \mu_0(j)) & := \bigcap_{(i,j) \in \D 1 \times J}B \cup \mu_0(j)\\
& := \bigcap_{(i,j) \in \D 1 \times J}\big(\lambda_0^B(i) \cup \mu_0(j)\big)\\
& =_{\C P(Y)} \bigg(\bigcap_{i \in \D 1}\lambda_0^B(i)\bigg) \cup \bigg(\bigcap_{j \in J}\mu_0(j)\bigg)\\
& =_{\C P(Y)} B \cup \bigg(\bigcap_{j \in J}\mu_0(j)\bigg).
\end{align*}

Let $X, Y, Z \in \D V_0$, $x_0 \in X, y_0 \in Y$, and $R(Z) := (\rho_0, \C E^Z \rho_1) \in \Fam(X \times Y, Z)$.

If $x \in X$, the $x$-component of $R$$x$-component of a family of subsets on $X \times Y$ is
the triplet$R^x(Z)$
$R^x(Z) := (\rho_0^x, \C E^{x,Z}, \rho_1^x)$, where the assignment routines $\rho_0^x, \rho_1^x$ are
as in Definition <ref>, and the dependent operation $\C E^{x,Z} \colon
\bigcurlywedge_{y \in Y}\D F\big(\rho_0^x(y), Z\big)$ is defined by
$\C E^{x,Z}_y := \C E_{(x,y)}^Z$, for every $y \in Y$.

If $y \in Y$, the $y$-component of $R$$y$-component of a family of subsets on $X \times Y$
is the triplet$R^y(Z)$
$R^y(Z) := (\rho_0^y, \C E^{y,Z}, \rho_1^y)$, where the assignment routines $\rho_0^y, \rho_1^y$ are
as in Definition <ref>, and the dependent operation $\C E^{y,Z} \colon
\bigcurlywedge_{x \in X}\D F\big(\rho_0^y(x), Z\big)$ is defined by
$\C E^{y,Z}_x := \C E_{(x,y)}^Z$, for every $x \in Y$.

Let $\bigcup^1R := (\bigcup^1 \rho_0, \big(\bigcup^1 \C E\big)^Z, \bigcup^1 \rho_1)$, where$\bigcup^1R$
$\bigcup^1 \rho_0 : X \sto \D V_0$,

\[\bigcup^1 \rho_1 \colon \bigcurlywedge_{(x, x{'}) \in D(X)}\D F\bigg(\big(\bigcup^1 \rho_0\big)(x),
\big(\bigcup^1 \rho_0\big)(x{'})\bigg),
\big(\bigcup^1 \C E\big)^Z \colon \bigcurlywedge_{x \in X}\D F\big(\big(\bigcup^1\rho_0\big)(x), Z\big)
\ \mbox{are defined by} \]

\[ \bigg(\bigcup^1 \rho_0\bigg) (x) := \bigcup_{y \in Y}\rho_0^x(y) := \bigcup_{y \in Y}\rho_0(x, y);
\ \ \ \ x \in X, \]

\[ \bigg(\bigcup^1 \rho_1\bigg) (x, x{'}) := \bigg(\bigcup^1 \rho_1\bigg)_{xx{'}} \colon
\bigcup_{y \in Y}\rho_0 (x, y) \to \bigcup_{y \in Y}\rho_0 (x{'}, y); \ \ \ \
(x, x{'}) \in D(X), \]

\[ \bigg(\bigcup^1 \rho_1\bigg)_{xx{'}}(y, u) := \big(y, \rho_{(x, y)(x{'},y)}(u)\big); \ \ \ \ (y, u) \in
\bigcup_{y \in Y}\rho_0 (x, y), \]

\[ \big(\bigcup^1 \C E\big)^Z_x (y, u) := \C E_{(x,y)}^Z(u); \ \ \ \ x \in X, \ (y, u) \in \bigcup_{y \in Y}\rho_0(x,y). \]

Let $\bigcup^2R := (\bigcup^2 \rho_0, \big(\bigcup^2 \C E\big)^Z, \bigcup^2 \rho_1)$, where$\bigcup^2R$
$\bigcup^2 \rho_0 : Y \sto \D V_0$,

\[\bigcup^2 \rho_1 \colon \bigcurlywedge_{(y, y{'}) \in D(Y)}\D F\bigg(\big(\bigcup^2 \rho_0\big)(x),
\big(\bigcup^2 \rho_0\big)(x{'})\bigg),
\big(\bigcup^2 \C E\big)^Z \colon \bigcurlywedge_{y \in Y}\D F\big(\big(\bigcup^2\rho_0\big)(y), Z\big)
\ \mbox{are defined by} \]

\[ \bigg(\bigcup^2 \rho_0\bigg) (y) := \bigcup_{x \in X}\rho_0^y(x) := \bigcup_{x \in X}\rho_0(x, y); \ \ \ \ y \in Y, \]

\[ \bigg(\bigcup^2 \rho_1\bigg) (y, y{'}) := \bigg(\bigcup^2 \rho_1\bigg)_{yy{'}} \colon
\bigcup_{x \in X}\rho_0 (x, y) \to \bigcup_{x \in X}\rho_0 (x{'}, y); \ \ \ \
(y, y{'}) \in D(Y), \]

\[ \bigg(\bigcup^2 \rho_1\bigg)_{yy{'}}(x, w) := \big(x, \rho_{(x, y)(x{'},y)}(w)\big); \ \ \ \ (x, w) \in
\bigcup_{x \in X}\rho_0 (x, y), \]

\[ \big(\bigcup^2 \C E\big)^Z_y (x, w) := \C E_{(x,y)}^Z(w); \ \ \ \ y \in Z, \ (x, w) \in \bigcup_{x \in X}\rho_0(x,y). \]

Let $\bigcap^1R := (\bigcap^1 \rho_0, \big(\bigcap^1 \C E\big)^Z, \bigcap^1 \rho_1)$, where$\bigcap^1R$
$\bigcap^1 \rho_0 : X \sto \D V_0$,

\[\bigcap^1 \rho_1 \colon \bigcurlywedge_{(x, x{'}) \in D(X)}\D F\bigg(\big(\bigcap^1 \rho_0\big)(x),
\big(\bigcap^1 \rho_0\big)(x{'})\bigg),
\big(\bigcap^1 \C E\big)^Z \colon \bigcurlywedge_{x \in X}\D F\big(\big(\bigcap^1\rho_0\big)(x), Z\big)
\ \mbox{are defined by} \]

\[ \bigg(\bigcap^1 \rho_0\bigg) (x) := \bigcap_{y \in Y}\rho_0^x(y) := \bigcap_{y \in Y}\rho_0(x, y); \ \ \ \ x \in X, \]

\[ \bigg(\bigcap^1 \rho_1\bigg) (x, x{'}) := \bigg(\bigcap^1 \rho_1\bigg)_{xx{'}} \colon
\bigcap_{y \in Y}\rho_0 (x, y) \to \bigcap_{y \in Y}\rho_0 (x{'}, y); \ \ \ \
(x, x{'}) \in D(X), \]

\[ \bigg[\bigg(\bigcap^1 \rho_1\bigg)_{xx{'}}(\Phi)\bigg]_y := \rho_{(x, y)(x{'},y)}(\Phi_y); \ \ \ \ \Phi \in
\bigcap_{y \in Y}\rho_0 (x, y), \]

\[ \big(\bigcap^1 \C E\big)^Z_x (\Phi) := \C E_{(x,y_0)}^Z(\Phi_{y_0}); \ \ \ \Phi \in \bigcap_{y \in Y}\rho_0(x,y). \]

Let $\bigcap^2R := (\bigcap^2 \rho_0, \big(\bigcap^2 \C E\big)^Z, \bigcap^2 \rho_1)$, where$\bigcap^2R$
$\bigcap^2 \rho_0 : X \sto \D V_0$,

\[\bigcap^2 \rho_1 \colon \bigcurlywedge_{(y, y{'}) \in D(Y)}\D F\bigg(\big(\bigcap^2 \rho_0\big)(y),
\big(\bigcap^2 \rho_0\big)(y{'})\bigg),
\big(\bigcap^2 \C E\big)^Z \colon \bigcurlywedge_{y \in Z}\D F\big(\big(\bigcap^2\rho_0\big)(y), Z\big)
\ \mbox{are defined by} \]

\[ \bigg(\bigcap^2 \rho_0\bigg) (y) := \bigcap_{x \in X}\rho_0^y(x) := \bigcap_{x \in X}\rho_0(x, y); \ \ \ \ y \in Y, \]

\[ \bigg(\bigcap^2 \rho_1\bigg) (y, y{'}) := \bigg(\bigcap^2 \rho_1\bigg)_{yy{'}} \colon
\bigcap_{x \in X}\rho_0 (x, y) \to \bigcap_{x \in X}\rho_0 (x, y{'}); \ \ \ \
(y, y{'}) \in D(Y), \]

\[ \bigg[\bigg(\bigcap^2 \rho_1\bigg)_{yy{'}}(\Phi)\bigg]_x := \rho_{(x, y)(x,y{'})}(\Phi_x); \ \ \ \ \Phi \in
\bigcap_{x \in X}\rho_0 (x, y), \]

\[ \big(\bigcap^2 \C E\big)^Z_y (\Phi) := \C E_{(x_0,y)}^Z(\Phi_{x_0}); \ \ \ \Phi \in \bigcap_{x \in X}\rho_0(x,y). \]

$R^y(Z), \bigcup^1R(Z), \bigcap^1R(Z)  \in \Fam(X, Z)$ and
$R^x(Z), \bigcup^2R(Z), \bigcap^2R(Z) \in \Fam(Y, Z)$.

Let $X, Y, Z \in \D V_0$, $R(Z) := (\rho_0, \C E^Z \rho_1), S(Z):= (\sigma_0, \C A^Z, \sigma_1)
\in \Fam(X \times Y, Z)$, and
$\Phi \colon R(Z) \To S(Z)$.

Let $\Phi^x \colon \bigcurlywedge_{y \in Y}\D F\big(\rho_0^x(y), \sigma_0^x(y)\big)$, where
$\Phi^x_y := \Phi_{(x,y)} \colon \rho_0^x(y) \to \sigma^x_0(y)$.

Let $\Phi^y \colon \bigcurlywedge_{x \in X}\D F\big(R^y(x), S^y(x)\big)$, where
$\Phi^y_x := \Phi_{(x,y)} \colon \rho_0^y(x) \to \sigma^y_0(x)$.

Let $\bigcup^1 \Phi \colon \bigcurlywedge_{x \in X}\D F\big(\big(\bigcup^1\rho_0\big)(x),
\big(\bigcup^1\sigma_0\big)(x)\big)$, where, for every $x \in X$, we define$\bigcup^1 \Phi$

\[ \bigg(\bigcup^1 \Phi\bigg)_x \colon \sum_{y \in Y}\rho_0^y(x) \to \bigcup_{y \in Y}\sigma^x_0(y) \]

\[ \bigg(\bigcup^1 \Phi\bigg)_x(y, u) := \big(y, \Phi_{(x,y)}(u)\big); \ \ \ \ (y, u) \in \bigcup_{y \in Y}\rho_0(x, y). \]

Let $\bigcup^2 \Phi \colon \bigcurlywedge_{y \in Y}\D F\big(\big(\bigcup^2\rho_0\big)(y),
\big(\bigcup^2\sigma_0\big)(y)\big)$, where, for every $y \in Y$, we define$\bigcup^2 \Phi$

\[ \bigg(\bigcup^2 \Phi\bigg)_y \colon \bigcup_{x \in X}\rho_0^x(y) \to \bigcup_{x \in X}\sigma^y_0(x) \]

\[ \bigg(\bigcup^2 \Phi\bigg)_y(x, w) := \big(x, \Phi_{(x,y)}(w)\big); \ \ \ \ (x, w) \in \bigcup_{x \in X}\rho(x, y). \]

Let $\bigcap^1 \Phi \colon \bigcurlywedge_{x \in X}\D F\big(\big(\bigcap^1\rho_0\big)(x),
\big(\bigcap^1\sigma_0\big)(x)\big)$, where, for every $x \in X$, we define$\bigcap^1 \Phi$

\[ \bigg(\bigcap^1 \Phi\bigg)_x \colon \bigcap_{y \in Y}\rho_0^y(x) \to \bigcap_{y \in Y}\sigma^x_0(y) \]

\[ \bigg[\bigg(\bigcap^1 \Phi\bigg)_x(\Theta)\bigg]_y := \Phi_{(x,y)}\big(\Theta_y))\big); \ \ \ \ \Theta \in
\bigcap_{y \in Y}\rho_0(x, y). \]

Let $\bigcap^2 \Phi \colon \bigcurlywedge_{y \in Y}\D F\big(\big(\bigcap^2\rho_0\big)(y),
\big(\bigcap^2\sigma_0\big)(y)\big)$, where, for every $y \in Y$, we define$\bigcap^2 \Phi$

\[ \bigg(\bigcap^2 \Phi\bigg)_y \colon \bigcap_{x \in X}\rho_0^x(y) \to \bigcap_{x \in X}\sigma^y_0(x) \]

\[ \bigg[\bigg(\bigcap^2 \Phi\bigg)_y(\Theta)\bigg]_x := \Phi_{(x,y)}\big(\Theta_x)\big); \ \ \ \ \Theta \in
\bigcap_{x \in X}\rho_0(x, y). \]

Then we have that $\Phi^x \colon R^x(Z) \To S^x(Z)$ and $\Phi^y \colon R^y(Z) \To S^y(Z)$ and
$\bigcup^1 \Phi \colon \big(\bigcup^1 R\big)(Z) \To \big(\bigcup^1 S\big)(Z)$ and
$\bigcup^2 \Phi \colon \big(\bigcup^2 R\big)(Z) \To \big(\bigcup^2 S\big)(Z)$ and
$\bigcap^1 \Phi \colon \big(\bigcap^1 R\big)(Z) \To \big(\bigcap^1 S\big)(Z)$ and
$\bigcap^2 \Phi \colon \big(\bigcap^2 R\big)(Z) \To \big(\bigcap^2 S\big)(Z)$.

We proceed similarly to the proof of Proposition <ref>.

If $R := (\rho_0, \rho_1) \in \Fam(X \times Y, Z)$, the following equalities hold.

\[ \bigcup_{x \in X}\bigcup_{y \in Y}\rho_0(x,y) =_{\C P(Z)} \bigcup_{y \in Y}\bigcup_{x \in X}\rho_0(x,y), \]

\[ \bigcap_{x \in X}\bigcap_{y \in Y}\rho_0(x,y) =_{\C P(Z)} \bigcap_{y \in Y}\bigcap_{x \in X}\rho_0(x,y). \]

The proof is straightforward.

§ THE SEMI-DISTRIBUTIVITY OF $\BIGCAP$ OVER $\BIGCUP$

Section <ref> is the “internal” analogue to section <ref>,
as the presentation of the families of subsets over products follows the presentation of the families
of sets over products.
The distributivity of $\bigcap$ over $\bigcup$ though, cannot be approached as the distributivity of
$\Sigma$ over $\prod$, as the crucial Lemma <ref> depends on the fact that the operation $\pr_1^{R^x}$ is a
function, something which is not the case, as we have already explained in section <ref>,
when the totality of the exterior union is equipped with the equality of the
interior union.

If $\Lambda(X) := (\lambda_0, \C E^X, \lambda_1) \in \Fam(I,X)$ and $h \colon J \to I$, the composition family

$\Lambda(X) \circ h$ of $\Lambda(X)$composition family of $\Lambda(X)$ with $h$
with $h$ is the triplet $\Lambda(X) \circ h := (\lambda_0 \circ h, \C E^X \circ h, \lambda_1 \circ h)$, where
$\lambda_0 \circ h \colon J \sto \D V_0$ and $\lambda_1 \circ h \colon \bigcurlywedge_{(j,j{'}) \in D(J)}
\D F\big(\lambda_0(h(j)), \lambda_0(h(j{'}))\big)$ are given in Definition <ref>$($iii$)$, and
the dependent operation $\C E^X \circ h \colon  \bigcurlywedge_{j \in J}\D F\big(\lambda_0(h(j)), X\big)$ is defined by
$(\C E^X \circ h)_j := \C E^X_{h(j)}$, for every $j \in J$.

Clearly, $\Lambda(X) \circ h \in \Fam(J, X)$. To formulate the distributivity of
$\bigcap$ over $\bigcup$ in the language of $\BST$ we need to introduce a family of subsets $P(I)$
of the index-set $I$ of a given family of subsets of a set $X$.
Throughout this section let the following data:

(a) $\Lambda(X) := (\lambda_0, \C E^X, \lambda_1) \in \Fam(I,X)$.

(b) $(K, =_K, \neq_K)$ is a set, and $k_0 \in K$.

(c) $P(I) := (p_0, \C Z^I, p_1) \in \Fam(K, I)$.

(d) $\Lambda(X) \circ \C Z^I_k := (\lambda_0 \circ \C Z^I_k, \C E^X \circ \C Z^I_k,
\lambda_1 \circ \C Z^I_k) \in
\Fam(p_0(k), X)$, for every $k \in K$.

(e) $T := \bigcap_{k \in K}p_0(k)$.

$N(K) := (\nu_0, \C N^X, \nu_1) \in \Fam(K, X)$, where $\nu_0 \colon K \sto \D V_0$ is defined by

\[\nu_0(k) := \bigcup_{j \in p_0(k)}(\lambda_0 \circ \C Z^I_k)(j) := \bigcup_{j \in p_0(k)}\lambda_0\big(\C Z^I_k(j)\big);
\ \ \  \ k \in K,
\]

and $\C N^X \colon \bigcurlywedge_{k \in K}\D F(\nu_0(k), X)$,
$\nu_1 \colon \bigcurlywedge_{(k,k{'}) \in D(K)}\D F\big(\nu_0(k), \nu_0(k{'})\big)$ are defined by

\[ \C N^X_k \colon \bigg(\bigcup_{j \in p_0(k)}\lambda_0\big(Z^I_k(j)\big)\bigg) \eto X, \ \
\C N^X_k(j, u) := \C E^X_{\C Z^I_k(j)}(u); \ \ \ \ j \in p_0(k), \ u \in \lambda_0\big(Z^I_k(j)\big), \]

\[ \nu_1(k, k{'}) := \nu_{kk{'}} \colon \bigcup_{j \in p_0(k)}\lambda_0\big(Z^I_k(j)\big) \to
\bigcup_{j \in p_0(k{'})}\lambda_0\big(Z^I_{k{'}}(j)\big), \]

\[ \nu_{kk{'}}(j, u) := \big(p_{kk{'}}(j), \lambda_{Z^I_k(j) Z^I_{k{'}}(p_{kk{'}}(j))}(u)\big); \ \ \ \
j \in p_0(k), \ u \in \lambda_0\big(Z^I_k(j)\big).
\]

The operation $\C N^X_k$ is an embedding, since by Definition <ref>

\[ (j, u) =_{\mathsmaller{\bigcup_{j \in p_0(k)}\lambda_0(Z^I_k(j))}} (j{'}, u{'}) :\TOT
\C E^X_{\C Z^I_k(j)}(u) =_X \C E^X_{\C Z^I_k(j{'})}(u{'}) :\TOT \C N^X_k(j, u) =_X \C N^X_k(j{'}, u{'}). \]

Let $k =_K k{'}$, $j \in p_0(k)$ and $u \in \lambda_0\big(Z^I_k(j)\big)$. By the commutativity of the left inner diagrams

(E) at (0,0) $p_0(k)$;
[right=of E] (B) ;
[right=of B] (F) $p_0(k{'})$;
[below=of B] (C) ;
[below=of C] (A) $I$;

[right=of F] (K) $\mathsmaller{\bigcup_{j \in p_0(k)}\lambda_0\big(Z^I_k(j)\big)}$;
[right=of K] (L) ;
[right=of L] (M) $\mathsmaller{\bigcup_{j{'} \in p_0(k{'})}\lambda_0\big(Z^I_{k{'}}(j{'})\big)}$;
[below=of L] (N) ;
[below=of N] (X) $X$;

[left hook->,bend left] (E) to node [midway,above] $p_{kk{'}}$ (F);
[left hook->,bend left] (F) to node [midway,below] $p_{k{'}k}$ (E);
[right hook->] (E)–(A) node [midway,left] $\C Z^I_k \ $;
[left hook->] (F)–(A) node [midway,right] $ \ \C Z^I_{k{'}}$;

[left hook->,bend left] (K) to node [midway,above] $\nu_{kk{'}}$ (M);
[left hook->,bend left] (M) to node [midway,below] $\nu_{k{'}k}$ (K);
[right hook->] (K)–(X) node [midway,left] $\C N^X_k \ $;
[left hook->] (M)–(X) node [midway,right] $ \ \C N^X_{k{'}}$;

we have that $\C Z^I_{k{'}}\big(p_{kk{'}}(j)\big) =_I \C Z^I_k(j)$. Hence $\lambda_{Z^I_k(j) Z^I_{k{'}}(p_{kk{'}}(j))}
\colon \lambda_0\big(\C Z^I_k(j)\big) \to \lambda_0\big(\C Z^I_{k{'}}\big(p_{kk{'}}(j)\big)\big)$ and
$\nu_{kk{'}}(j, u)$ is well defined. Next we show that the above right inner diagrams commute. If

\[ j{'} := p_{kk{'}}(j) \ \ \& \ \ i :=  Z^I_k(j) \ \ \& \ \ i{'} := \C Z^I_{k{'}}(j{'}), \ \ \ \ \mbox{then} \]

\[ \C N^X_{k{'}}\big(\nu_{kk{'}}(j, u)\big) := \C N^X_{k{'}}\big(j{'}, \lambda_{ii{'}}(u)\big) :=
\C E^X_{i{'}}\big( \lambda_{ii{'}}(u)\big) =_X \C E^X_i(u) := \C N^X_{k}(j,u), \]

using the commutativity of the following diagram

(E) at (0,0) $\lambda_0(i)$;
[right=of E] (B) ;
[right=of B] (F) $\lambda_0(i{'})$;
[below=of B] (C) ;
[below=of C] (A) $X$.;

[left hook->,bend left] (E) to node [midway,above] $\lambda_{ii{'}}$ (F);
[left hook->,bend left] (F) to node [midway,below] $\lambda_{i{'}i}$ (E);
[right hook->] (E)–(A) node [midway,left] $\C E^X_i \ $;
[left hook->] (F)–(A) node [midway,right] $ \ \C E^X_{i{'}}$;

For the other above right inner diagram we proceed similarly. Clearly, $\nu_{kk}(j, u) := (j, u)$.

If $\tau \in T$, then
$\tau(X) := (\tau_0, \C T^X, \tau_1) \in \Fam(K, X)$, where $\tau_0 \colon K \sto \D V_0$ is defined by
$\tau_0(k) := \lambda_0\big(\C Z^I_k(\tau_k)\big)$, for every $k \in K$, and the dependent operations
$\C T^X \colon \bigcurlywedge_{k \in K}\D F(\tau_0(k), X)$,
$\tau_1 \colon \bigcurlywedge_{(k,k{'}) \in D(K)}\D F\big(\tau_0(k), \tau_0(k{'})\big)$ are defined by

\[ \C T^X_k \colon\lambda_0\big( \C Z^I_k(\tau_k)\big) \eto X, \ \
\C T^ X_k := \C E^X_{\C Z^I_k(\tau_k)},  \]

\[ \tau_1(k, k{'}) := \tau_{kk{'}} \colon \lambda_0\big(\C Z^I_k(\tau_k)\big) \to
\lambda_0\big(\C Z^I_{k{'}}(\tau_{k{'}})\big), \ \ \ \ \tau_{kk{'}} := \lambda_{Z^I_k(\tau_k) Z^I_{k{'}}(\tau_{k{'}})}.
\]

What we want follows in a straightforward way from the fact that $\Lambda(X) \in \Fam(I, X)$.

$\Xi (X) := (\xi_0, \C H^X, \xi_1) \in \Fam(T, X)$, where $\xi_0 \colon T \sto \D V_0$ is defined by

\[ \xi_0(\tau) := \bigcap_{k \in K}\tau_0(k) := \bigcap_{k \in K}\lambda_0\big(\C Z_k^I(\tau_k)\big); \ \ \ \ \tau \in T,\]

and the dependent operations
$\C H^X \colon \bigcurlywedge_{\tau \in T}\D F(\xi_0(\tau), X)$,
$\xi_1 \colon \bigcurlywedge_{(\tau,\tau{'}) \in D(T)}\D F\big(\xi_0(\tau), \xi_0(\tau{'})\big)$ are defined, respectively, by
$\C H^X_{\tau} \colon \bigg(\bigcap_{k \in K}\tau_0(k)\bigg) \eto X$, where $\C H_{\tau}^X := e_{\mathsmaller{\bigcap}}^{\tau(X)}$, for every $\tau \in T$,

\[ \xi_1(\tau, \tau{'}) := \xi_{\tau \tau{'}} \colon \bigcap_{k \in K}\lambda_0\big(\C Z_k^I(\tau_k)\big) \to
\bigcap_{k \in K}\lambda_0\big(\C Z_k^I(\tau{'}_k)\big),\]

\[ \Phi \mapsto \xi_{\tau \tau{'}}(\Phi); \ \ \ \ \big[\xi_{\tau \tau{'}}(\Phi)\big]_k := \lambda_{\C Z_k^I(\tau_k)\C Z_k^I(\tau{'}_k)}(\Phi_k); \ \ \ \ \Phi \colon \bigcap_{k \in K}\lambda_0\big(\C Z_k^I(\tau_k)\big), \   k \in K.\]

If $\tau \in T$, then by the definition of the embedding $e_{\mathsmaller{\bigcap}}^{\tau(X)}$ we get

\[ \C H_{\tau}^X(\Phi) := \C T_{k_0}^X(\Phi_{k_0}) := \C E_{\C Z_{k_0}^I(\tau_{k_0})}^X(\Phi_{k_0}); \ \ \ \
\Phi \colon \bigcap_{k \in K}\lambda_0\big(\C Z_k^I(\tau_k)\big).\]

$\C H^X_{\tau}$ is an embedding. Next we show that $\xi_{\tau \tau{'}}(\Phi) \in
\bigcap_{k \in K}\lambda_0\big(\C Z_k^I(\tau{'}_k)\big)$. As $\Phi \colon
\bigcap_{k \in K}\lambda_0\big(\C Z_k^I(\tau_k)\big)$,

\begin{align*}
\C T_k^X\big(\big[\xi_{\tau \tau{'}}(\Phi)\big]_k\big) & := \C E^X_{\C Z^I_k(\tau{'}_k)}\bigg(\big[\xi_{\tau \tau{'}}(\Phi)\big]_k\bigg)\\
& := \C E^X_{\C Z^I_k(\tau{'}_k)}\bigg(\lambda_{\C Z_k^I(\tau_k)\C Z_k^I(\tau{'}_k)}(\Phi_k)\bigg)\\
& =_X \C E^X_{\C Z^I_k(\tau_k)}(\Phi_k)\\
& =_X \C E^X_{\C Z^I_l(\tau_l)}(\Phi_l)\\
& =_X \C E^X_{\C Z^I_l(\tau{'}_l)}\bigg(\lambda_{\C Z_k^I(\tau_l)\C Z_k^I(\tau{'}_l)}(\Phi_l)\bigg)\\
& := \C T_l^X\big(\big[\xi_{\tau \tau{'}}(\Phi)\big]_l\big),
\end{align*}

for every $k, l \in K$. Similarly we show that $\xi_{\tau \tau{'}}$ is a function. If $\tau =_T \tau{'}$, then

(E) at (0,0) $\bigcap_{k \in K}\lambda_0(\C Z_k^I(\tau_k)))$;
[right=of E] (B) ;
[right=of B] (F) $\bigcap_{k \in K}\lambda_0(\C Z^I_k(\tau{'}_k))$;
[below=of B] (C) ;
[below=of C] (A) $X$;

[left hook->,bend left] (E) to node [midway,above] $\xi_{\tau \tau{'}}$ (F);
[left hook->,bend left] (F) to node [midway,below] $\xi_{\tau{'}\tau}$ (E);
[right hook->] (E)–(A) node [midway,left] $\C H^X_{\tau} \ $;
[left hook->] (F)–(A) node [midway,right] $ \ \C H^X_{\tau{'}}$;

\begin{align*}
\C H^X_{\tau{'}}\big(\xi_{\tau \tau{'}}(\Phi)\big) & := \C E_{\C Z_{k_0}^I(\tau{'}_{k_0})}^X\bigg(\big[\xi_{\tau \tau{'}}(\Phi)\big]_{k_0}\bigg)\\
& := \C E_{\C Z_{k_0}^I(\tau{'}_{k_0})}^X\bigg( \lambda_{\C Z_{k_0}^I(\tau_{k_0})\C Z_{k_0}^I(\tau{'}_{k_0})}(\Phi_{k_0})  \bigg)\\
& =_X \C E_{\C Z_{k_0}^I(\tau_{k_0})}^X\big(\Phi_{k_0}\big)\\
& := \C H_{\tau}^X(\Phi).\qedhere
\end{align*}

The set

\[ W:= \bigcap_{k \in K}\nu_0(k) := \bigcap_{k \in K}\bigg[\bigcup_{j \in p_0(k)}\lambda_0\big(\C Z^I_k(j)\big)\bigg]\]

is embedded into $X$ through the map $e_{\mathsmaller{\bigcap}}^{N(X)}$, where $e_{\mathsmaller{\bigcap}}^{N(X)}(A) := \C N^X_{k_0}(A_{k_0})$, for every $A \in \bigcap_{k \in K}\nu_0(k)$. By definition, if $A \colon \bigcurlywedge_{k \in K}\nu_0(k)$, then

\[ A \in \bigcap_{k \in K}\nu_0(k) \TOT \forall_{k,l \in K}\big(\C N^X_k(A_k) =_X \C N^X_l(A_l)\big), \]