chap-alt-bin.tex

\chapter{Alternative representations of binary relations}

\begin{thm}
Let $A$ and~$B$ be fixed sets. The diagram at the figure~\ref{rels-dia} is
a commutative diagram (in category $\mathbf{Set}$), every arrow in
this diagram is an isomorphism. Every cycle in this diagram is an
identity. All ``parallel'' arrows are mutually inverse.

For a Galois connection~$f$ I denote $f_0$ the lower adjoint and $f_1$ the upper adjoint.
For simplicity, in the diagram I equate $\subsets A$ and $\mathscr{T}A$.

\begin{figure}[ht]
\begin{tikzcd}[row sep=1cm, column sep=-1.0cm]
& \begin{tabular}{c}binary relations\\ between $A$ and $B$\end{tabular}
\arrow[rd, shift left, "\Psi_1^{-1}"]
\arrow[ld, shift left, "\Psi_2"] \\
\begin{tabular}{c}pointfree funcoids\\ between\\ $\subsets A$ and $\subsets B$\end{tabular}
\arrow[ru, shift left, "\Psi_2^{-1}"]
\arrow[rr, shift left, "\Psi_3"]
\arrow[rd, shift left, "\Psi_4"]
& & \begin{tabular}{c}antitone Galois\\ connections\\ between\\ $\subsets A$ and $\subsets B$\end{tabular}
\arrow[lu, shift left, "\Psi_1"]
\arrow[ll, shift left, "\Psi_3^{-1}"]
\arrow[ld, leftrightarrow, "\Psi_5=\Psi_5^{-1}"]
\\
& \begin{tabular}{c}Galois connections\\ between $\subsets A$ and $\subsets B$\end{tabular}
\arrow[lu, shift left, "\Psi_4^{-1}"]
\end{tikzcd}

\begin{flushleft}
\begin{description}
\item[$\Psi_1$] $f\mapsto\setcond{(x,y)}{y\in f_0\{x\}}=\setcond{(x,y)}{x\in f_1\{y\}}$
\item[$\Psi_1^{-1}$] $r\mapsto\left(X\mapsto\setcond{y\in B}{\forall x\in X:x\mathrel{r}y}, Y\mapsto\setcond{x\in A}{\forall y\in Y:x\mathrel{r}y}\right)$
\item[$\Psi_2$] $r\mapsto(\subsets A,\subsets B,\rsupfun{r},\rsupfun{r^{-1}})$
\item[$\Psi_2^{-1}$] $f\mapsto\setcond{(x,y)}{\{x\}\suprel{f}\{y\}}$
\item[$\Psi_3$] $f\mapsto\left(X\mapsto\bigsqcap_{x\in\mathscr{T} X\setminus\{\bot\}}\supfun{f}x,Y\mapsto\bigsqcap_{y\in\mathscr{T} Y\setminus\{\bot\}}\supfun{f^{-1}}y\right)=
  \left(X\mapsto\bigsqcap_{x\in X}\supfun{f}\{x\},Y\mapsto\bigsqcap_{y\in Y}\supfun{f^{-1}}\{y\}\right)$
\item[$\Psi_3^{-1}$] $f\mapsto\left(\subsets A,\subsets B,X\mapsto\bigsqcup_{x\in\mathscr{T}X\setminus\{\bot\}}f_0 x,Y\mapsto\bigsqcup_{y\in\mathscr{T}Y\setminus\{\bot\}}f_1 y\right)=
  \left(\subsets A,\subsets B,X\mapsto\bigsqcup_{x\in X}f_0\{x\},Y\mapsto\bigsqcup_{y\in Y}f_1\{y\}\right)$
\item[$\Psi_4$] $f\mapsto\left(X\mapsto\lnot\bigsqcap_{x\in\mathscr{T} X\setminus\{\bot\}}\supfun{f}x,Y\mapsto\bigsqcap_{y\in\mathscr{T} Y\setminus\{\bot\}}\supfun{f^{-1}}\lnot y\right)=
  \left(X\mapsto\bigsqcup_{x\in\mathscr{T}X\setminus\{\bot\}}\lnot\supfun{f}x,Y\mapsto\bigsqcap_{y\in\mathscr{T} Y\setminus\{\bot\}}\supfun{f^{-1}}\lnot y\right)=
  \left(X\mapsto\lnot \bigsqcap_{x\in X}\supfun{f}\{x\},Y\mapsto\bigsqcap_{y\in Y}\supfun{f^{-1}}\lnot \{y\}\right)=
  \left(X\mapsto\bigsqcup_{x\in X}\lnot\supfun{f}\{x\},Y\mapsto\bigsqcap_{y\in Y}\supfun{f^{-1}}\lnot \{y\}\right)$
\item[$\Psi_4^{-1}$] $f\mapsto\left(\subsets A,\subsets B,X\mapsto\bigsqcup_{x\in\mathscr{T}X\setminus\{\bot\}}\lnot f_0 x,Y\mapsto\bigsqcup_{y\in\mathscr{T}Y\setminus\{\bot\}}f_1\lnot y\right)=
  \left(\subsets A,\subsets B,X\mapsto\lnot\bigsqcap_{x\in\mathscr{T}X\setminus\{\bot\}}f_0 x,Y\mapsto\bigsqcup_{y\in\mathscr{T}Y\setminus\{\bot\}}f_1\lnot y\right)=
  \left(\subsets A,\subsets B,X\mapsto\bigsqcup_{x\in X}\lnot f_0\{x\},Y\mapsto\bigsqcup_{y\in Y}f_1\lnot\{y\}\right)=
  \left(\subsets A,\subsets B,X\mapsto\lnot\bigsqcap_{x\in X}f_0\{x\},Y\mapsto\bigsqcup_{y\in Y}f_1\lnot\{y\}\right)$
\item[$\Psi_5=\Psi_5^{-1}$] $f\mapsto(\mathord{\lnot}\circ f_0,f_1\circ\mathord{\lnot})$
\end{description}
\end{flushleft}

\caption{\label{rels-dia}}
\end{figure}
\end{thm}

\begin{proof}
First, note that despite we use the notation~$\Psi_i^{-1}$, it is not yet proved that~$\Psi_i^{-1}$ is the inverse of~$\Psi_i$. We will prove it below.

Now prove a list of claims. First concentrate on the upper ``triangle'' of the diagram (the lower one will be considered later).

\begin{claim}
$\setcond{(x,y)}{y\in f_0\{x\}}=\setcond{(x,y)}{x\in f_1\{y\}}$ when $f$ is an antitone Galois connection between~$\subsets A$ and~$\subsets B$.
\end{claim}
\begin{claimproof}
$y\in f_0\{x\}\Leftrightarrow\{y\}\sqsubseteq f_0\{x\}\Leftrightarrow\{x\}\sqsubseteq f_1\{y\}\Leftrightarrow x\in f_1\{y\}$.
\end{claimproof}

\begin{claim}
$\scriptstyle \left(X\mapsto\bigsqcap_{x\in\mathscr{T} X\setminus\{\bot\}}\supfun{f}x,Y\mapsto\bigsqcap_{y\in\mathscr{T} Y\setminus\{\bot\}}\supfun{f^{-1}}y\right)=
\left(X\mapsto\bigsqcap_{x\in X}\supfun{f}\{x\},Y\mapsto\bigsqcap_{y\in Y}\supfun{f^{-1}}\{y\}\right)$
when $f$ is a pointfree funcoid between~$\subsets A$ and~$\subsets B$.
\end{claim}
\begin{claimproof}
It is enough to prove $\bigsqcap_{x\in\mathscr{T} X\setminus\{\bot\}}\supfun{f}x = \bigsqcap_{x\in X}\supfun{f}\{x\}$ (the rest follows from symmetry).
$\bigsqcap_{x\in\mathscr{T} X\setminus\{\bot\}}\supfun{f}x \sqsubseteq \bigsqcap_{x\in X}\supfun{f}\{x\}$ because
$\mathscr{T} X\setminus\{\bot\}\supseteq\setcond{\{x\}}{x\in X}$.
$\bigsqcap_{x\in\mathscr{T} X\setminus\{\bot\}}\supfun{f}x \sqsupseteq \bigsqcap_{x\in X}\supfun{f}\{x\}$ because
if $x\in\mathscr{T} X\setminus\{\bot\}$ then we can take $x'\in x$ that is $\{x'\}\subseteq x$ and thus
$\supfun{f}x \sqsupseteq \supfun{f}\{x'\}$, so
$\bigsqcap_{x\in\mathscr{T} X\setminus\{\bot\}}\supfun{f}x \sqsupseteq \bigsqcap_{x\in\mathscr{T} X\setminus\{\bot\}}\supfun{f}\{x'\} \sqsupseteq
\bigsqcap_{x\in X}\supfun{f}\{x\}$.
\end{claimproof}

\begin{flushleft}
\begin{claim}
$\left(\subsets A,\subsets B,X\mapsto\bigsqcup_{x\in\mathscr{T}X\setminus\{\bot\}}f_0 x,Y\mapsto\bigsqcup_{y\in\mathscr{T}Y\setminus\{\bot\}}f_1 y\right) =
\left(\subsets A,\subsets B,X\mapsto\bigsqcup_{x\in X}f_0\{x\},Y\mapsto\bigsqcup_{y\in Y}f_1\{y\}\right)$
when $f$ is an antitone Galois connection between~$\subsets A$ and~$\subsets B$.
\end{claim}
\end{flushleft}
\begin{claimproof}
It is enough to prove $\bigsqcup_{x\in\mathscr{T}X\setminus\{\bot\}}f_0 x=\bigsqcup_{x\in X}f_0\{x\}$ (the rest follows from symmetry).
We have $\bigsqcup_{x\in\mathscr{T}X\setminus\{\bot\}}f_0 x\sqsupseteq\bigsqcup_{x\in X}f_0\{x\}$ because $\{x\}\in\mathscr{T}X\setminus\{\bot\}$.
Let $x\in\mathscr{T}X\setminus\{\bot\}$. Take $x'\in X$. We have $f_0 x\sqsubseteq f_0\{x'\}$ and thus
$f_0 x\sqsubseteq \bigsqcup_{x\in X}f_0\{x\}$. So $\bigsqcup_{x\in\mathscr{T}X\setminus\{\bot\}}f_0 x\sqsubseteq\bigsqcup_{x\in X}f_0\{x\}$.
\end{claimproof}

\begin{claim}
$\Psi_3^{-1} = \Psi_2\circ\Psi_1$.
\end{claim}
\begin{claimproof}
$\Psi_2\Psi_1 f = \left(\subsets A,\subsets B,X\mapsto\setcond{y}{\exists x\in X:(x,y)\in\Psi_1 f},Y\mapsto\setcond{x}{\exists y\in Y:(x,y)\in\Psi_1 f}\right) =
\left(\subsets A,\subsets B,X\mapsto\setcond{y}{\exists x\in X:y\in f_0\{x\}},Y\mapsto\setcond{x}{\exists y\in Y:x\in f_1\{y\}}\right) =
\left(\subsets A,\subsets B,X\mapsto\bigsqcup_{x\in X}f_0\{x\},Y\mapsto\bigsqcup_{y\in Y}f_1\{y\}\right) =
\Psi_3^{-1} f$.
\end{claimproof}

\begin{claim}
$\Psi_3 = \Psi_1^{-1}\circ\Psi_2^{-1}$.
\end{claim}
\begin{claimproof}
$\Psi_1^{-1}\Psi_2^{-1} f = 
\left(X\mapsto\setcond{y\in B}{\forall x\in X:\{x\}\suprel{f}\{y\}}, Y\mapsto\setcond{x\in A}{\forall y\in Y:\{x\}\suprel{f}\{y\}}\right) =
\left(X\mapsto\setcond{y\in B}{\forall x\in X:y\in\supfun{f}\{x\}}, Y\mapsto\setcond{x\in A}{\forall y\in Y:x\in\supfun{f^{-1}}\{y\}}\right) =
\left(X\mapsto\bigsqcap_{x\in X}\supfun{f}\{x\},Y\mapsto\bigsqcap_{y\in Y}\supfun{f^{-1}}\{y\}\right) = \Psi_3 f$.
\end{claimproof}

\begin{claim}
$\Psi_1$ maps antitone Galois connections between~$\subsets A$ and~$\subsets B$ into binary relations between~$A$ and~$B$.
\end{claim}
\begin{claimproof}
Obvious.
\end{claimproof}

\begin{claim}
$\Psi_1^{-1}$ maps binary relations between~$A$ and~$B$ into antitone Galois connections between~$\subsets A$ and~$\subsets B$.
\end{claim}
\begin{claimproof}
We need to prove $Y\subseteq\setcond{y\in B}{\forall x\in X:x\mathrel{r}y}\Leftrightarrow X\subseteq\setcond{x\in A}{\forall y\in Y:x\mathrel{r}y}$.
After we equivalently rewrite it:
\[\forall y\in Y \forall x\in X:x\mathrel{r}y\Leftrightarrow\forall x\in X\forall y\in Y:x\mathrel{r}y\]
it becomes obvious.
\end{claimproof}

\begin{claim}
$\Psi_2$ maps binary relations between~$A$ and~$B$ into pointfree funcoids between~$\subsets A$ and~$\subsets B$.
\end{claim}
\begin{claimproof}
We need to prove that $f=(\subsets A,\subsets B,\supfun{f},\supfun{f^{-1}})$ is a pointfree funcoids that is $Y\nasymp\supfun{f}X\Leftrightarrow X\nasymp\supfun{f^{-1}}Y$. Really, for every
$X\in\mathscr{T}A$, $Y\in\mathscr{T}B$ 
\begin{multline*}
Y\nasymp\supfun fX\Leftrightarrow Y\nasymp\rsupfun rX\Leftrightarrow Y\nasymp\supfun rX\Leftrightarrow\\
X\nasymp\supfun{r^{-1}}Y\Leftrightarrow X\nasymp\rsupfun{r^{-1}}Y\Leftrightarrow X\nasymp\supfun{f^{-1}}Y.
\end{multline*}
\end{claimproof}

\begin{claim}
$\Psi_2^{-1}$ maps pointfree funcoids between~$\subsets A$ and~$\subsets B$ into binary relations between~$A$ and~$B$.
\end{claim}
\begin{claimproof}
Suppose $f\in\mathsf{pFCD}(\mathscr{T}A,\mathscr{T}B)$ and prove
that the relation defined by the formula~$\Psi_2^{-1}$ exists.
To prove it, it's enough to show that $y\in\supfun f\{x\}\Leftrightarrow x\in\supfun{f^{-1}}\{y\}$.
Really, 
\[
y\in\supfun f\{x\}\Leftrightarrow\{y\}\nasymp\supfun f\{x\}\Leftrightarrow\{x\}\nasymp\supfun{f^{-1}}\{y\}\Leftrightarrow x\in\supfun{f^{-1}}\{y\}.
\]
\end{claimproof}

\begin{claim}
$\Psi_3$ maps pointfree funcoids between~$\subsets A$ and~$\subsets B$ into antitone Galois connections between~$\subsets A$ and~$\subsets B$.
\end{claim}
\begin{claimproof}
Because $\Psi_3 = \Psi_1^{-1}\circ\Psi_2^{-1}$.
\end{claimproof}

\begin{claim}
$\Psi_3^{-1}$ maps antitone Galois connections between~$\subsets A$ and~$\subsets B$ into pointfree funcoids between~$\subsets A$ and~$\subsets B$.
\end{claim}
\begin{claimproof}
Because $\Psi_3^{-1} = \Psi_2\circ\Psi_1$.
\end{claimproof}

\begin{claim}
$\Psi_2$ and $\Psi_2^{-1}$ are mutually inverse.
\end{claim}
\begin{claimproof}
Let $r_{0}\in\subsets(A\times B)$ and $f\in\mathsf{pFCD}(\mathscr{T}A,\mathscr{T}B)$
corresponds to~$r_{0}$ by the formula~$\Psi_2$; let $r_{1}\in\subsets(A\times B)$
corresponds to~$f$ by the formula~$\Psi_2^{-1}$. Then $r_{0}=r_{1}$
because 
\[
(x,y)\in r_{0}\Leftrightarrow y\in\rsupfun{r_{0}}\{x\}\Leftrightarrow y\in\supfun f\{x\}\Leftrightarrow(x,y)\in r_{1}.
\]

Let now $f_{0}\in\mathsf{pFCD}(\mathscr{T}A,\mathscr{T}B)$ and $r\in\subsets(A\times B)$
corresponds to~$f_{0}$ by the formula~$\Psi_2^{-1}$; let $f_{1}\in\mathsf{pFCD}(\mathscr{T}A,\mathscr{T}B)$
corresponds to~$r$ by the formula~$\Psi_2$. Then $(x,y)\in r\Leftrightarrow y\in\supfun{f_{0}}\{x\}$
and $\supfun{f_{1}}=\rsupfun r$; thus 
\[
y\in\supfun{f_{1}}\{x\}\Leftrightarrow y\in\rsupfun r\{x\}\Leftrightarrow(x,y)\in r\Leftrightarrow y\in\supfun{f_{0}}\{x\}.
\]
So $\supfun{f_{0}}=\supfun{f_{1}}$. Similarly $\supfun{f_{0}^{-1}}=\supfun{f_{1}^{-1}}$.
\end{claimproof}

\begin{claim}
$\Psi_1$ and $\Psi_1^{-1}$ are mutually inverse.
\end{claim}
\begin{claimproof}
Let $r_0\in\subsets(A\times B)$ and $f\in\mathscr{T}A\otimes\mathscr{T}B$
corresponds to~$r_{0}$ by the formula~$\Psi_1^{-1}$; let $r_{1}\in\subsets(A\times B)$
corresponds to~$f$ by the formula~$\Psi_1$. Then $r_{0}=r_{1}$ because
\[
(x,y)\in r_1 \Leftrightarrow y\in f_0\{x\} \Leftrightarrow y\in\setcond{y\in B}{x\mathrel{r_0}y} \Leftrightarrow x\mathrel{r_0}y.
\]

Let now $f_{0}\in\mathscr{T}A\otimes\mathscr{T}B$ and $r\in\subsets(A\times B)$
corresponds to~$f_{0}$ by the formula~$\Psi_1$; let $f_{1}\in\mathscr{T}A\otimes\mathscr{T}B$
corresponds to~$r$ by the formula~$\Psi_1^{-1}$. Then $f_0=f_1$ because
\begin{multline*}
f_{10} X = \setcond{y\in B}{\forall x\in X:x\mathrel{r}y} = \setcond{y\in B}{\forall x\in X:y\in f_{00}\{x\}} = \\
\bigsqcap_{x\in X}f_{00}\{x\} = \text{(obvious~\ref{polar-flip})} = f_{00}X.
\end{multline*}
\end{claimproof}

\begin{claim}
$\Psi_3$ and $\Psi_3^{-1}$ are mutually inverse.
\end{claim}
\begin{claimproof}
Because $\Psi_3^{-1} = \Psi_2\circ\Psi_1$ and $\Psi_3 = \Psi_1^{-1}\circ\Psi_2^{-1}$
and that $\Psi_2^{-1}$ is the inverse of $\Psi_2$ and $\Psi_3^{-1}$ is the inverse of $\Psi_3$ were proved above.
\end{claimproof}

Now switch to the lower ``triangle'':

\begin{flushleft}
\begin{claim}
$\left(X\mapsto\bigsqcup_{x\in\mathscr{T}X\setminus\{\bot\}}\lnot f_0 x,Y\mapsto\bigsqcup_{y\in\mathscr{T}Y\setminus\{\bot\}}f_1\lnot y\right)=\left(X\mapsto\bigsqcup_{x\in X}\lnot f_0\{x\},Y\mapsto\bigsqcup_{y\in Y}f_1\lnot\{y\}\right)$.
\end{claim}
\end{flushleft}
\begin{claimproof}
It is enough to prove $\bigsqcup_{x\in\mathscr{T}X\setminus\{\bot\}}\lnot f_0 x = \bigsqcup_{x\in X}\lnot f_0\{x\}$ for a Galois connection~$f$
(the rest follows from symmetry).

$\bigsqcup_{x\in\mathscr{T}X\setminus\{\bot\}}\lnot f_0 x \sqsupseteq \bigsqcup_{x\in X}\lnot f_0\{x\}$ because $\{x\}\in\mathscr{T}X\setminus\{\bot\}$.
If $x\in\mathscr{T}X\setminus\{\bot\}$ then there exists $x'\in\{x\}$ and thus $\lnot f_0\{x'\}\sqsupseteq \lnot f_0 x$. Thus
$\lnot f_0 x \sqsubseteq \bigsqcup_{x\in X} \lnot f_0 \{x\}$ and so
$\bigsqcup_{x\in\mathscr{T}X\setminus\{\bot\}}\lnot f_0 x \sqsubseteq \bigsqcup_{x\in X}\lnot f_0\{x\}$.
\end{claimproof}

\begin{claim}
$\Psi_5$ is self-inverse.
\end{claim}
\begin{claimproof}
Obvious.
\end{claimproof}

\begin{claim}
$\Psi_4 = \Psi_5\circ\Psi_3$.
\end{claim}
\begin{claimproof}
Easily follows from symmetry.
\end{claimproof}

\begin{claim}
$\Psi_4^{-1} = \Psi_3^{-1}\circ\Psi_5^{-1}$.
\end{claim}
\begin{claimproof}
Easily follows from symmetry.
\end{claimproof}

\begin{claim}
$\Psi_4$ and $\Psi_4^{-1}$ are mutually inverse.
\end{claim}
\begin{claimproof}
From two above claims and the fact that
$\Psi_3^{-1}$ is the inverse of $\Psi_3$ and $\Psi_5^{-1}$ is the inverse of $\Psi_5$ proved above.
\end{claimproof}

Note that now we have proved that $\Psi_i$ and $\Psi_i^{-1}$ are mutually inverse for all $i=1,2,3,4,5$.

\begin{claim}
For every path of the diagram on figure~\ref{rels-dia2} started with the circled node, the corresponding morphism is with which the node is labeled.
\begin{figure}[ht]
\begin{tikzcd}[row sep=1cm, column sep=0.5cm]
& \circled{1}
\arrow[rd, shift left, "\Psi_1^{-1}"]
\arrow[ld, shift left, "\Psi_2"] \\
\Psi_2
\arrow[ru, shift left, "\Psi_2^{-1}"]
\arrow[rr, shift left, "\Psi_3"]
\arrow[rd, shift left, "\Psi_4"]
& & \Psi_1^{-1}
\arrow[lu, shift left, "\Psi_1"]
\arrow[ll, shift left, "\Psi_3^{-1}"]
\arrow[ld, leftrightarrow, "\Psi_5=\Psi_5^{-1}"]
\\
& \Psi_5\circ\Psi_1^{-1}
\arrow[lu, shift left, "\Psi_4^{-1}"]
\end{tikzcd}
\caption{\label{rels-dia2}}
\end{figure}
\end{claim}
\begin{claimproof}
Take into account that $\Psi_3^{-1} = \Psi_2\circ\Psi_1$, $\Psi_4 = \Psi_5\circ\Psi_3$
and thus also $\Psi_4\circ\Psi_2 = \Psi_5\circ\Psi_1^{-1}$.
Now prove it by induction on path length.
\end{claimproof}

\begin{claim}
Every cycle in the diagram at figure~\ref{rels-dia} is identity.
\end{claim}
\begin{claimproof}
For cycles starting at the top node it follows from the previous claim.
For arbitrary cycles it follows from theorem~\ref{rehash-isos}.
\end{claimproof}

\begin{claim}
The diagram at figure~\ref{rels-dia} is commutative.
\end{claim}
\begin{claimproof}
From the previous claim.
\end{claimproof}

\end{proof}

\begin{prop}
We equate the set of binary relations between~$A$ and~$B$ with $\mathbf{Rld}(A,B)$.
$\Psi_2$ and~$\Psi_2^{-1}$ from the diagram at figure~\ref{rels-dia} preserve composition and identities (that are functors
between categories $\mathbf{Rel}$ and $(A,B)\mapsto\mathsf{pFCD}(\mathscr{T}A,\mathscr{T}B)$) and also reversal ($f\mapsto f^{-1}$).
\end{prop}

\begin{proof}
Let $\supfun f=\rsupfun p$ and $\supfun g=\rsupfun q$. Then $\supfun{g\circ f}=\supfun g\circ\supfun f=\rsupfun q\circ\rsupfun p=\rsupfun{q\circ p}$.
Likewise $\supfun{(g\circ f)^{-1}}=\rsupfun{(q\circ p)^{-1}}$. So
$\Phi_2$ preserves composition.

Let $p=1_{\mathbf{Rel}}^{A}$ for some set~$A$. Then $\supfun f=\rsupfun p=\rsupfun{1_{\mathbf{Rel}}^{A}}=\id_{\subsets A}$
and likewise $\supfun{f^{-1}}=\id_{\subsets A}$, that is $f$ is
an identity pointfree funcoid. So $\Phi_2$ preserves identities.

That $\Phi_2^{-1}$ preserves composition and identities follows from the fact that it is an isomorphism.

That is preserves reversal follows from the formula $\supfun{f^{-1}}=\rsupfun{p^{-1}}$.
\end{proof}

\begin{prop}
The bijections $\Psi_2$ and~$\Psi_2^{-1}$ from the diagram at figure~\ref{rels-dia} preserves monovaluedness
and injectivity.\end{prop}
\begin{proof}
Because it is a functor which preserves reversal.\end{proof}
\begin{prop}
The bijections $\Psi_2$ and~$\Psi_2^{-1}$ from the diagram at figure~\ref{rels-dia} preserves domain
an image.\end{prop}
\begin{proof}
$\im f=\supfun f\top=\rsupfun p\top=\im p$, likewise for domain.\end{proof}
\begin{prop}
The bijections $\Psi_2$ and~$\Psi_2^{-1}$ from the diagram at figure~\ref{rels-dia} maps cartesian
products to corresponding funcoidal products.\end{prop}
\begin{proof}
$\supfun{A\times^{\mathsf{FCD}}B}X=\begin{cases}
B & \text{if }X\nasymp A\\
\bot & \text{if }X\asymp A
\end{cases}=\rsupfun{A\times B}X$. Likewise $\supfun{(A\times^{\mathsf{FCD}}B)^{-1}}Y=\rsupfun{(A\times B)^{-1}}Y$.\end{proof}

Let $\Phi$ map a pointfree funcoid whose first component is~$c$ into the Galois connection whose lower adjoint is~$c$.
Then $\Phi$ is an isomorphism (theorem~\ref{bfunc-is-adj}) and
$\Phi^{-1}$ maps a Galois connection whose lower adjoint is~$c$ into the pointfree funcoid whose first component is~$c$.

Informally speaking, $\Phi$ replaces a relation~$r$ with its complement relations~$\lnot r$. Formally:

\begin{prop}
~
\begin{enumerate}
\item For every path~$P$ in the diagram at figure~\ref{rels-dia} from binary relations between $A$ and $B$
to pointfree funcoids between $\subsets A$ and $\subsets B$
and every path~$Q$ in the diagram at figure~\ref{rels-dia} from
Galois connections between $\subsets A$ and $\subsets B$
to binary relations between $A$ and $B$,
we have $Q\Phi P r = \lnot r$.

\item For every path~$Q$ in the diagram at figure~\ref{rels-dia} from binary relations between $A$ and $B$
to pointfree funcoids between $\subsets A$ and $\subsets B$
and every path~$P$ in the diagram at figure~\ref{rels-dia}
from Galois connections between $\subsets A$ and $\subsets B$
to binary relations between $A$ and $B$,
we have $P\Phi^{-1} Q r = \lnot r$.
\end{enumerate}
\end{prop}

\begin{proof}
We will prove only the second ($P\circ \Phi^{-1}\circ Q = \lnot$), because the first ($Q\circ\Phi\circ P= \lnot$)
can be obtained from it by inverting the morphisms (and variable replacement).

Because the diagram is commutative, it is enough to prove it for some fixed~$P$ and~$Q$.
For example, we will prove $\Psi_2^{-1} \Phi^{-1} \Psi_4 \Psi_2 r = \neg r$.

$\Psi_4 \Psi_2 r = \left( X \mapsto \neg \bigsqcap_{x \in X} \rsupfun{r}
\{ x \} , Y \mapsto \bigsqcap_{y \in Y} \rsupfun{r} \neg \{ y \} \right)$.

$\Phi^{-1} \Psi_4 \Psi_2 r$ is pointfree funcoid $f$ with $\supfun{f}
= X \mapsto \neg \bigsqcap_{x \in X} \rsupfun{r} \{ x \}$.

$\Psi_2^{-1} \Phi^{-1} \Psi_4 \Psi_2 r$ is the relation consisting of $(x ,
y)$ such that $\{ x \} \suprel{f} \{ y \}$ what is equivalent to: $\{ y \}
\nasymp \supfun{f} \{ x \}$; $\{ y \} \nasymp \neg \rsupfun{r} \{ x \}$; $\{ y \} \nsqsubseteq \rsupfun{r} \{ x \}$; $y \notin \rsupfun{r} \{ x \}$.

So $\Psi_2^{-1} \Phi^{-1} \Psi_4 \Psi_2 r = \neg r$.
\end{proof}

\begin{prop}
$\Phi$ and $\Phi^{-1}$ preserve composition.
\end{prop}

\begin{proof}
By definitions of compositions and the fact that both pointfree funcoids and Galois connections are determined by the first component.
\end{proof}