chap-rel.tex

\chapter{\texorpdfstring{Typed sets and category $\mathbf{Rel}$}%
{Typed sets and category Rel}}


\section{Relational structures}
\begin{defn}
\index{relational structure}A \emph{relational structure} is a pair
consisting of a set and a tuple of relations on this set.
\end{defn}
A poset $(\mathfrak{A},\sqsubseteq)$ can be considered as a relational
structure: $(\mathfrak{A},\llbracket\sqsubseteq\rrbracket).$

A set can $X$ be considered as a relational structure with zero relations:
$(X,\llbracket\rrbracket).$

This book is not about relational structures. So I will not introduce
more examples.

Think about relational structures as a common place for sets or posets,
as far as they are considered in this book.

We will denote $x\in(\mathfrak{A},R)$ iff $x\in\mathfrak{A}$ for
a relational structure $(\mathfrak{A},R)$.


\section{Typed elements and typed sets}

We sometimes want to differentiate between the same element of two
different sets. For example, we may want to consider different the
natural number~$3$ and the rational number~$3$. In order to describe
this in a formal way we consider elements of sets together with sets
themselves. For example, we can consider the pairs $(\mathbb{N},3)$
and $(\mathbb{Q},3)$.
\begin{defn}
\index{typed element}\index{element!typed}A \emph{typed element}
is a pair $(\mathfrak{A},a)$ where $\mathfrak{A}$ is a relational
structure and $a\in\mathfrak{A}$.

I denote $\type(\mathfrak{A},a)=\mathfrak{A}$ and $\GR(\mathfrak{A},a)=a$.
\end{defn}

\begin{defn}
I will denote typed element $(\mathfrak{A},a)$ as $@^{\mathfrak{A}} a$ or just
$@a$ when $\mathfrak{A}$ is clear from context.
\end{defn}

\begin{defn}
\index{typed set}\index{set!typed}A \emph{typed set} is a typed
element equal to $(\subsets U,A)$ where $U$ is a set and $A$ is
its subset.\end{defn}
\begin{rem}
\emph{Typed sets} is an awkward formalization of type theory sets
in ZFC ($U$ is meant to express the \emph{type} of the set). This
book could be better written using type theory instead of ZFC, but
I want my book to be understandable for everyone knowing ZFC. $(\subsets U,A)$
should be understood as a set $A$ of type $U$. For an example, consider
$(\subsets\mathbb{R},[0;10])$; it is the closed interval $[0;10]$
whose elements are considered as real numbers.\end{rem}
\begin{defn}
$\mathfrak{T}\mathfrak{A}=\setcond{(\mathfrak{A},a)}{a\in\mathfrak{A}}=\{\mathfrak{A}\}\times\mathfrak{A}$
for every relational structure~$\mathfrak{A}$.\end{defn}
\begin{rem}
$\mathfrak{T}\mathfrak{A}$ is the set of typed elements of~$\mathfrak{A}$.
\end{rem}

\begin{defn}
If $\mathfrak{A}$ is a poset, we introduce order on its typed elements
isomorphic to the order of the original poset: $(\mathfrak{A},a)\sqsubseteq(\mathfrak{A},b)\Leftrightarrow a\sqsubseteq b$.
\end{defn}

\begin{defn}
I denote $\GR(\mathfrak{A},a)=a$ for a typed element~$(\mathfrak{A},a)$.
\end{defn}

\begin{defn}
I will denote \emph{typed subsets} of a typed poset $(\subsets U,A)$
as $\subsets(\subsets U,A)=\setcond{(\subsets U,X)}{X\in\subsets A}=\{\subsets U\}\times\subsets A$.\end{defn}
\begin{obvious}
$\subsets(\subsets U,A)$ is also a set of typed sets.
\end{obvious}

\begin{defn}
I will denote $\mathscr{T}U=\mathfrak{T}\subsets U$.\end{defn}
\begin{rem}
This means that $\mathscr{T}U$ is the set of typed subsets of a set~$U$.\end{rem}
\begin{obvious}
$\mathscr{T}U=\setcond{(\subsets U,X)}{X\in\subsets U}=\{\subsets U\}\times\subsets U=\subsets(\subsets U,U)$.
\end{obvious}

\begin{obvious}
$\mathscr{T}U$ is a complete atomistic boolean lattice. Particularly:
\begin{enumerate}
\item $\bot^{\mathscr{T}U}=(\subsets U,\emptyset)$;
\item $\top^{\mathscr{T}U}=(\subsets U,U)$;
\item $(\subsets U,A)\sqcup(\subsets U,B)=(\subsets U,A\cup B)$;
\item $(\subsets U,A)\sqcap(\subsets U,B)=(\subsets U,A\cap B)$;
\item $\bigsqcup_{A\in S}(\subsets U,A)=(\subsets U,\bigcup_{A\in S}A)$;
\item $\bigsqcap_{A\in S}(\subsets U,A)=\left(\subsets U,\begin{cases}\bigcap_{A\in S}A&\text{ if }A\ne\emptyset\\U&\text{ if }A=\emptyset\end{cases}\right)$;
\item $\overline{(\subsets U,A)}=(\subsets U,U\setminus A)$;
\item atomic elements are $(\subsets U,\{x\})$ where $x\in U$.
\end{enumerate}
Typed sets are ``better'' than regular sets as (for example) for
a set~$U$ and a typed set~$X$ the following are defined by regular
order theory:\end{obvious}
\begin{itemize}
\item $\atoms X$;
\item $\overline{X}$;
\item $\bigsqcap^{\mathscr{T}U}\emptyset$.
\end{itemize}
For regular (``non-typed'') sets these are not defined (except of
$\atoms X$ which however needs a special definition instead of using
the standard order-theory definition of atoms).

Typed sets are convenient to be used together with filters on sets
(see below), because both typed sets and filters have a set~$\subsets U$
as their type.

Another advantage of typed sets is that their binary product (as defined
below) is a $\mathbf{Rel}$-morphism. This is especially convenient
because below defined products of filters are also morphisms of related
categories.

Well, typed sets are also quite awkward, but the proper way of doing
modern mathematics is \emph{type theory} not ZFC, what is however
outside of the topic of this book.


\section{\texorpdfstring{Category $\mathbf{Rel}$}{Category Rel}}

I remind that $\mathbf{Rel}$ is the category of (small) binary relations
between sets, and $\mathbf{Set}$ is its subcategory where only monovalued
entirely defined morphisms (functions) are considered.
\begin{defn}
Order on $\mathbf{Rel}(A,B)$ is defined by the formula $f\sqsubseteq g\Leftrightarrow\GR f\subseteq\GR g$.\end{defn}
\begin{obvious}
This order is isomorphic to the natural order of subsets of the set
$A\times B$.\end{obvious}
\begin{defn}
$X\rsuprel fY\Leftrightarrow\GR X\rsuprel{\GR f}\GR Y$ and $\rsupfun fX=(\Dst f,\rsupfun{\GR f}\GR X)$
for a $\mathbf{Rel}$-morphism~$f$ and typed sets $X\in\mathscr{T}\Src f$,
$Y\in\mathscr{T}\Dst f$.
\end{defn}

\begin{defn}
For category $\mathbf{Rel}$ there is defined reverse morphism: $(A,B,F)^{-1}=(B,A,F^{-1})$.\end{defn}
\begin{obvious}
$(f^{-1})^{-1}=f$ for every $\mathbf{Rel}$-morphism~$f$.
\end{obvious}

\begin{obvious}
$\rsuprel{f^{-1}}=\rsuprel f^{-1}$ for every $\mathbf{Rel}$-morphism~$f$.
\end{obvious}

\begin{obvious}
$(g\circ f)^{-1}=f^{-1}\circ g^{-1}$ for every composable $\mathbf{Rel}$-morphisms
$f$ and~$g$.\end{obvious}
\begin{prop}
$\rsupfun{g\circ f}=\rsupfun g\circ\rsupfun f$ for every composable
$\mathbf{Rel}$-morphisms $f$ and~$g$.\end{prop}
\begin{proof}
Exercise.\end{proof}
\begin{prop}
The above definitions of monovalued morphisms of $\mathbf{Rel}$ and
of injective morphisms of $\mathbf{Set}$ coincide with how mathematicians
usually define monovalued functions (that is morphisms of $\mathbf{Set}$)
and injective functions.\end{prop}
\begin{proof}
Let $f$ be a $\mathbf{Rel}$-morphism $A\rightarrow B$.

The following are equivalent:
\begin{itemize}
\item $f$ is a monovalued relation;
\item $\forall x\in A,y_{0},y_{1}\in B:(x\mathrel fy_{0}\land x\mathrel fy_{1}\Rightarrow y_{0}=y_{1})$;
\item $\forall x\in A,y_{0},y_{1}\in B:(y_{0}\ne y_{1}\Rightarrow\lnot(x\mathrel fy_{0})\lor\lnot(x\mathrel fy_{1}))$;
\item $\forall y_{0},y_{1}\in B\forall x\in A:(y_{0}\ne y_{1}\Rightarrow\lnot(x\mathrel fy_{0})\lor\lnot(x\mathrel fy_{1}))$;
\item $\forall y_{0},y_{1}\in B:(y_{0}\ne y_{1}\Rightarrow\forall x\in A:(\lnot(x\mathrel fy_{0})\lor\lnot(x\mathrel fy_{1})))$;
\item $\forall y_{0},y_{1}\in B:(\exists x\in A:(x\mathrel fy_{0}\land x\mathrel fy_{1})\Rightarrow y_{0}=y_{1})$;
\item $\forall y_{0},y_{1}\in B:y_{0}\mathrel{(f\circ f^{-1})}y_{1}\Rightarrow y_{0}=y_{1}$;
\item $f\circ f^{-1}\sqsubseteq1_{B}$.
\end{itemize}
Let now $f$ be a $\mathbf{Set}$-morphism $A\rightarrow B$.

The following are equivalent:
\begin{itemize}
\item $f$ is an injective function;
\item $\forall y\in B,a,b\in A:(a\mathrel fy\land b\mathrel fy\Rightarrow a=b)$;
\item $\forall y\in B,a,b\in A:(a\ne b\Rightarrow\lnot(a\mathrel fy)\lor\lnot(b\mathrel fy))$;
\item $\forall y\in B:(a\ne b\Rightarrow\forall a,b\in A:(\lnot(a\mathrel fy)\lor\lnot(b\mathrel fy)))$;
\item $\forall y\in B:(\exists a,b\in A:(a\mathrel fy\land b\mathrel fy)\Rightarrow a=b)$;
\item $f^{-1}\circ f\sqsubseteq1_{A}$.
\end{itemize}
\end{proof}
\begin{prop}
For a binary relation $f$ we have:
\begin{enumerate}
\item \label{br-j}$\rsupfun f\bigcup S=\bigcup\rsupfun{\rsupfun f}S$ for
a set of sets $S$;
\item \label{br-j1}$\bigcup S\rsuprel fY\Leftrightarrow\exists X\in S:X\rsuprel fY$
for a set of sets $S$;
\item \label{br-j2}$X\rsuprel f\bigcup T\Leftrightarrow\exists Y\in T:X\rsuprel fY$
for a set of sets $T$;
\item \label{br-j12}$\bigcup S\rsuprel f\bigcup T\Leftrightarrow\exists X\in S,Y\in T:X\rsuprel fY$
for sets of sets $S$ and $T$;
\item \label{br-at-r}$X\rsuprel fY\Leftrightarrow\exists\alpha\in X,\beta\in Y:\{\alpha\}\rsuprel f\{\beta\}$
for sets $X$ and $Y$;
\item \label{br-at-f}$\rsupfun fX=\bigcup\rsupfun{\rsupfun f}\atoms X$ for a
set $X$ (where $\atoms X=\setcond{\{x\}}{x\in X}$).
\end{enumerate}
\end{prop}
\begin{proof}
~
\begin{widedisorder}
\item [{\ref{br-j}}] ~

\begin{multline*}
y\in\rsupfun f\bigcup S\Leftrightarrow\exists x\in\bigcup S:x\mathrel fy\Leftrightarrow\exists P\in S,x\in P:x\mathrel fy\Leftrightarrow\\
\exists P\in S:y\in\rsupfun fP\Leftrightarrow\exists Q\in\rsupfun{\rsupfun f}S:y\in Q\Leftrightarrow y\in\bigcup\rsupfun{\rsupfun f}S.
\end{multline*}

\item [{\ref{br-j1}}] 
\begin{multline*}
\bigcup S\rsuprel fY\Leftrightarrow\exists x\in\bigcup S,y\in Y:x\mathrel fy\Leftrightarrow\\
\exists X\in S,x\in X,y\in Y:x\mathrel fy\Leftrightarrow\exists X\in S:X\rsuprel fY.
\end{multline*}

\item [{\ref{br-j2}}] By symmetry.
\item [{\ref{br-j12}}] From two previous formulas.
\item [{\ref{br-at-r}}] $X\rsuprel fY\Leftrightarrow\exists\alpha\in X,\beta\in Y:\alpha\mathrel f\beta\Leftrightarrow\exists\alpha\in X,\beta\in Y:\{\alpha\}\rsuprel f\{\beta\}$.
\item [\ref{br-at-f}] Obvious.
\end{widedisorder}
\end{proof}
\begin{cor}
For a $\mathbf{Rel}$-morphism $f$ we have:
\begin{enumerate}
\item $\rsupfun f\bigsqcup S=\bigsqcup\rsupfun{\rsupfun f}S$ for $S\in\subsets\mathscr{T}\Src f$;
\item $\bigsqcup S\rsuprel fY\Leftrightarrow\exists X\in S:X\rsuprel fY$
for $S\in\subsets\mathscr{T}\Src f$;
\item $X\rsuprel f\bigsqcup T\Leftrightarrow\exists Y\in T:X\rsuprel fY$
for $T\in\subsets\mathscr{T}\Dst f$;
\item $\bigsqcup S\rsuprel f\bigsqcup T\Leftrightarrow\exists X\in S,Y\in T:X\rsuprel fY$
for $S\in\subsets\mathscr{T}\Src f$, $T\in\subsets\mathscr{T}\Dst f$;
\item $X\rsuprel fY\Leftrightarrow\exists x\in\atoms X,y\in\atoms Y:x\rsuprel fy$
for $X\in\mathscr{T}\Src f$, $Y\in\mathscr{T}\Dst f$;
\item $\rsupfun fX=\bigsqcup\rsupfun{\rsupfun f}\atoms X$ for $X\in\mathscr{T}\Src f$.
\end{enumerate}
\end{cor}

\begin{cor}
A $\mathbf{Rel}$-morphism $f$ can be restored knowing either $\rsupfun fx$
for atoms $x\in\mathscr{T}\Src f$ or $x\rsuprel fy$ for atoms $x\in\mathscr{T}\Src f$,
$y\in\mathscr{T}\Dst f$.\end{cor}
\begin{prop}
Let $A$, $B$ be sets, $R$ be a set of binary relations.
\begin{enumerate}
\item \textbf{\label{bsr-jf}$\rsupfun{\bigcup R}X=\bigcup_{f\in R}\rsupfun fX$}
for every set $X$;
\item \label{bsr-mf}$\rsupfun{\bigcap R}\{\alpha\}=\bigcap_{f\in R}\rsupfun f\{\alpha\}$
for every $\alpha$, if $R$ is nonempty;
\item \label{bsr-jr}$X\rsuprel{\bigcup R}Y\Leftrightarrow\exists f\in R:X\rsuprel fY$
for every sets $X$, $Y$;
\item \label{bsr-mr}$\alpha\mathrel{\left(\bigcap R\right)}\beta\Leftrightarrow\forall f\in R:\alpha\mathrel f\beta$
for every $\alpha$ and $\beta$, if $R$ is nonempty.
\end{enumerate}
\end{prop}
\begin{proof}
~
\begin{widedisorder}
\item [{\ref{bsr-jf}}] ~
\begin{multline*}
y\in\rsupfun{\bigcup R}X\Leftrightarrow\exists x\in X:x\mathrel{\left(\bigcup R\right)}y\Leftrightarrow\exists x\in X,f\in R:x\mathrel fy\Leftrightarrow\\
\exists f\in R:y\in\rsupfun fX\Leftrightarrow y\in\bigcup_{f\in R}\rsupfun fX.
\end{multline*}

\item [{\ref{bsr-mf}}] ~ 
\[
y\in\rsupfun{\bigcap R}\{\alpha\}\Leftrightarrow\forall f\in R:\alpha\mathrel fy\Leftrightarrow\forall f\in R:y\in\rsupfun f\{\alpha\}\Leftrightarrow y\in\bigcap_{f\in R}\rsupfun f\{\alpha\}.
\]

\item [{\ref{bsr-jr}}] ~
\begin{multline*}
X\rsuprel{\bigcup R}Y\Leftrightarrow\exists x\in X,y\in Y:x\mathrel{\left(\bigcup R\right)}y\Leftrightarrow\\
\exists x\in X,y\in Y,f\in R:x\mathrel fy\Leftrightarrow\exists f\in R:X\rsuprel fY.
\end{multline*}

\item [{\ref{bsr-mr}}] Obvious.
\end{widedisorder}
\end{proof}
\begin{cor}
Let $A$, $B$ be sets, $R\in\subsets\mathbf{Rel}(A,B)$.
\begin{enumerate}
\item \textbf{$\rsupfun{\bigsqcup R}X=\bigsqcup_{f\in R}\rsupfun fX$} for
$X\in\mathscr{T}A$;
\item $\rsupfun{\bigsqcap R}x=\bigsqcap_{f\in R}\rsupfun fx$ for atomic
$x\in\mathscr{T}A$;
\item $X\rsuprel{\bigsqcup R}Y\Leftrightarrow\exists f\in R:X\rsuprel fY$
for $X\in\mathscr{T}A$, $Y\in\mathscr{T}B$;
\item $x\rsuprel{\bigsqcap R}y\Leftrightarrow\forall f\in R:x\rsuprel fy$
for every atomic $x\in\mathscr{T}A$, $y\in\mathscr{T}B$.
\end{enumerate}
\end{cor}
\begin{prop}
$X\rsuprel{g\circ f}Z\Leftrightarrow\exists\beta:(X\rsuprel f\{\beta\}\land\{\beta\}\rsuprel gZ)$
for every binary relation~$f$ and sets $X$ and $Y$.\end{prop}
\begin{proof}
~
\begin{multline*}
X\rsuprel{g\circ f}Z\Leftrightarrow\exists x\in X,z\in Z:x\mathrel{(g\circ f)}z\Leftrightarrow\\
\exists x\in X,z\in Z,\beta:(x\mathrel f\beta\land\beta\mathrel gz)\Leftrightarrow\\
\exists\beta:(\exists x\in X:x\mathrel f\beta\land\exists y\in Y:\beta\mathrel gz)\Leftrightarrow\exists\beta:(X\rsuprel f\{\beta\}\land\{\beta\}\rsuprel gZ).
\end{multline*}
\end{proof}
\begin{cor}
$X\rsuprel{g\circ f}Z\Leftrightarrow\exists y\in\atoms^{\mathscr{T}B}:(X\rsuprel fy\land y\rsuprel gZ)$
for $f\in\mathbf{Rel}(A,B)$, $g\in\mathbf{Rel}(B,C)$ (for sets $A$,
$B$, $C$).\end{cor}
\begin{prop}
$f\circ\bigcup G=\bigcup_{g\in G}(f\circ g)$ and $\bigcup G\circ f=\bigcup_{g\in G}(g\circ f)$
for every binary relation~$f$ and set~$G$ of binary relations.\end{prop}
\begin{proof}
We will prove only $\bigcup G\circ f=\bigcup_{g\in G}(g\circ f)$
as the other formula follows from duality. Really

\begin{multline*}
(x,z)\in\bigcup G\circ f\Leftrightarrow\exists y:((x,y)\in f\land(y,z)\in\bigcup G)\Leftrightarrow\\
\exists y,g\in G:((x,y)\in f\land(y,z)\in g)\Leftrightarrow\exists g\in G:(x,z)\in g\circ f\Leftrightarrow(x,z)\in\bigcup_{g\in G}(g\circ f).
\end{multline*}
\end{proof}
\begin{cor}
Every $\mathbf{Rel}$-morphism is metacomplete and co-metacomplete.\end{cor}
\begin{prop}
\label{rel-mono}The following are equivalent for a $\mathbf{Rel}$-morphism~$f$:
\begin{enumerate}
\item \label{rel-mono-mono}$f$ is monovalued.
\item \label{rel-mmv}$f$ is metamonovalued.
\item \label{rel-wmmv}$f$ is weakly metamonovalued.
\item \label{rel-mono-atom}$\rsupfun fa$ is either atomic or least whenever
$a\in\atoms^{\mathscr{T}\Src f}$.
\item \label{rel-mono-bin}$\rsupfun{f^{-1}}(I\sqcap J)=\rsupfun{f^{-1}}I\sqcap\rsupfun{f^{-1}}J$
for every $I,J\in\mathscr{T}\Src f$.
\item \label{rel-mono-meet}$\rsupfun{f^{-1}}\bigsqcap S=\bigsqcap_{Y\in S}\rsupfun{f^{-1}}Y$
for every $S\in\subsets\mathscr{T}\Src f$.
\end{enumerate}
\end{prop}
\begin{proof}
~
\begin{description}
\item [{\ref{rel-mmv}$\Rightarrow$\ref{rel-wmmv}}] Obvious.
\item [{\ref{rel-mono-mono}$\Rightarrow$\ref{rel-mmv}}] Take $x\in\atoms^{\mathscr{T}\Src f}$;
then $fx\in\atoms^{\mathscr{T}\Dst f}\cup\{\bot^{\mathscr{T}\Dst f}\}$ and thus 
\begin{multline*}
\rsupfun{\left(\bigsqcap G\right)\circ f}x=\rsupfun{\bigsqcap G}\rsupfun fx=\bigsqcap_{g\in G}\rsupfun g\rsupfun fx=\\
\bigsqcap_{g\in G}\rsupfun{g\circ f}x=\rsupfun{\bigsqcap_{g\in G}(g\circ f)}x;
\end{multline*}
so $\left(\bigsqcap G\right)\circ f=\bigsqcap_{g\in G}(g\circ f)$.
\item [{\ref{rel-wmmv}$\Rightarrow$\ref{rel-mono-mono}}] Take $g=\{(a,y)\}$
and $h=\{(b,y)\}$ for arbitrary $a\ne b$ and arbitrary~$y$. We
have $g\cap h=\emptyset$; thus $(g\circ f)\cap(h\circ f)=(g\cap h)\circ f=\bot$
and thus impossible $x\mathrel fa\land x\mathrel fb$ as otherwise
$(x,y)\in(g\circ f)\cap(h\circ f)$. Thus $f$ is monovalued.
\item [{\ref{rel-mono-atom}$\Rightarrow$\ref{rel-mono-meet}}] Let $a\in\atoms^{\mathscr{T}\Src f}$,
$\rsupfun fa=b$. Then because $b\in\atoms^{\mathscr{T}\Dst f}\cup\{\bot^{\mathscr{T}\Dst f}\}$
\begin{gather*}
\bigsqcap S\sqcap b\ne\bot\Leftrightarrow\forall Y\in S:Y\sqcap b\ne\bot;\\
a\rsuprel f\bigsqcap S\Leftrightarrow\forall Y\in S:a\rsuprel fY;\\
\bigsqcap S\rsuprel{f^{-1}}a\Leftrightarrow\forall Y\in S:Y\rsuprel{f^{-1}}a;\\
a\nasymp\rsupfun{f^{-1}}\bigsqcap S\Leftrightarrow\forall Y\in S:a\nasymp\rsupfun{f^{-1}}Y;\\
a\nasymp\rsupfun{f^{-1}}\bigsqcap S\Leftrightarrow a\nasymp\bigsqcap_{Y\in S}\rsupfun{f^{-1}}Y;\\
\rsupfun{f^{-1}}\bigsqcap S=\bigsqcap_{X\in S}\rsupfun{f^{-1}}X.
\end{gather*}

\item [{\ref{rel-mono-meet}$\Rightarrow$\ref{rel-mono-bin}}] Obvious.
\item [{\ref{rel-mono-bin}$\Rightarrow$\ref{rel-mono-mono}}]
$\rsupfun{f^{-1}}a\sqcap\rsupfun{f^{-1}}b=\rsupfun{f^{-1}}(a\sqcap b)=\rsupfun{f^{-1}}\bot=\bot$
for every two distinct atoms $a=\{\alpha\},b=\{\beta\}\in\mathscr{T}\Dst f$.
From this 
\begin{multline*}
\alpha\mathrel{(f\circ f^{-1})}\beta\Leftrightarrow\exists y\in\Dst f:(\alpha\mathrel{f^{-1}}y\land y\mathrel{f}\beta)\Leftrightarrow\\
\exists y\in\Dst f:(y\in\rsupfun{f^{-1}}a\land y\in\rsupfun{f^{-1}}b)
\end{multline*}
 is impossible. Thus $f\circ f^{-1}\sqsubseteq1_{\Dst f}^{\mathbf{Rel}}$.
\item [{$\lnot$\ref{rel-mono-atom}$\Rightarrow\lnot$\ref{rel-mono-mono}}] Suppose
$\rsupfun fa\notin\atoms^{\mathscr{T}\Dst f}\cup\{\bot^{\mathscr{T}\Dst f}\}$
for some $a\in\atoms^{\mathscr{T}\Src f}$. Then there exist distinct
points $p$, $q$ such that $p,q\in\rsupfun fa$. Thus $p\mathrel{(f\circ f^{-1})}q$
and so $f\circ f^{-1}\nsqsubseteq1_{\Dst f}^{\mathbf{Rel}}$.
\end{description}
\end{proof}

\section{Product of typed sets}
\begin{defn}
Product of typed sets is defined by the formula
\[
(\subsets U,A)\times(\subsets W,B)=(U,W,A\times B).
\]
\end{defn}
\begin{prop}
Product of typed sets is a $\mathbf{Rel}$-morphism.\end{prop}
\begin{proof}
We need to prove $A\times B\subseteq U\times W$, but this is obvious.\end{proof}
\begin{obvious}
Atoms of $\mathbf{Rel}(A,B)$ are exactly products $a\times b$ where
$a$ and $b$ are atoms correspondingly of $\mathscr{T}A$ and $\mathscr{T}B$.
$\mathbf{Rel}(A,B)$ is an atomistic poset.\end{obvious}
\begin{prop}
$f\nasymp A\times B\Leftrightarrow A\rsuprel fB$ for every $\mathbf{Rel}$-morphism~$f$
and $A\in\mathscr{T}\Src f$, $B\in\mathscr{T}\Dst f$.\end{prop}
\begin{proof}
~
\begin{multline*}
A\rsuprel fB\Leftrightarrow\exists x\in\atoms A,y\in\atoms B:x\rsuprel fy\Leftrightarrow\\
\exists x\in\atoms^{\mathscr{T}\Src f},y\in\atoms^{\mathscr{T}\Dst f}:(x\times y\sqsubseteq f\land x\times y\sqsubseteq A\times B)\Leftrightarrow f\nasymp A\times B.
\end{multline*}
\end{proof}
\begin{defn}
\emph{Image} and \emph{domain} of a $\mathbf{Rel}$-morphism~$f$
are typed sets defined by the formulas 
\[
\dom(U,W,f)=(\subsets U,\dom f)\quad\text{and}\quad\im(U,W,f)=(\subsets W,\im f).
\]
\end{defn}
\begin{obvious}
Image and domain of a $\mathbf{Rel}$-morphism are really typed sets.\end{obvious}
\begin{defn}
\emph{Restriction} of a $\mathbf{Rel}$-morphism to a typed set is
defined by the formula $(U,W,f)|_{(\subsets U,X)}=(U,W,f|_{X})$.\end{defn}
\begin{obvious}
Restriction of a $\mathbf{Rel}$-morphism is $\mathbf{Rel}$-morphism.
\end{obvious}

\begin{obvious}
$f|_{A}=f\sqcap(A\times\top^{\mathscr{T}\Dst f})$ for every $\mathbf{Rel}$-morphism~$f$
and $A\in\mathscr{T}\Src f$.
\end{obvious}

\begin{obvious}
$\rsupfun fX=\rsupfun f(X\sqcap\dom f)=\im(f|_{X})$ for every $\mathbf{Rel}$-morphism~$f$
and $X\in\mathscr{T}\Src f$.
\end{obvious}

\begin{obvious}
$f\sqsubseteq A\times B\Leftrightarrow\dom f\sqsubseteq A\land\im f\sqsubseteq B$
for every $\mathbf{Rel}$-morphism~$f$ and $A\in\mathscr{T}\Src f$,
\textbf{$B\in\mathscr{T}\Dst f$}.\end{obvious}
\begin{thm}
Let $A$, $B$ be sets. If $S\in\subsets(\mathscr{T}A\times\mathscr{T}B)$
then
\[
\bigsqcap_{(A,B)\in S}(A\times B)=\bigsqcap\dom S\times\bigsqcap\im S.
\]
\end{thm}
\begin{proof}
For every atomic $x\in\mathscr{T}A$, $y\in\mathscr{T}B$ we have
\begin{multline*}
x\times y\sqsubseteq\bigsqcap_{(A,B)\in S}(A\times B)\Leftrightarrow\forall(A,B)\in S:x\times y\sqsubseteq A\times B\Leftrightarrow\\
\forall(A,B)\in S:(x\sqsubseteq A\land y\sqsubseteq B)\Leftrightarrow\forall A\in\dom S:x\sqsubseteq A\land\forall B\in\im S:y\sqsubseteq B\Leftrightarrow\\
x\sqsubseteq\bigsqcap\dom S\land y\sqsubseteq\bigsqcap\im S\Leftrightarrow x\times y\sqsubseteq\bigsqcap\dom S\times\bigsqcap\im S.
\end{multline*}
\end{proof}
\begin{obvious}
If $U$, $W$ are sets and $A\in\mathscr{T}(U)$ then $A\times$ is
a complete homomorphism from the lattice $\mathscr{T}(W)$ to the
lattice $\mathbf{Rel}(U,W)$, if also $A\ne\bot$
then it is an order embedding.\end{obvious}