text:
\section{Introduction}

With each compact Hausdorff space $X$, we can associate numerous algebraic structures that determine $X$ up to homeomorphism. This
yields various dualities for the category ${\mathsf{KHaus}}$ of compact Hausdorff spaces and continuous maps. In this paper we are interested in two dualities for ${\mathsf{KHaus}}$ from pointfree topology. By Isbell duality \cite{Isb72}, ${\mathsf{KHaus}}$ is dually equivalent to the category ${\mathsf{KRFrm}}$ of compact regular frames and frame homomorphisms; and by de Vries duality \cite{deV62}, ${\mathsf{KHaus}}$ is dually equivalent to the category ${\mathsf{DeV}}$ of de Vries algebras and de Vries morphisms.

Isbell duality is established by working with the contravariant functor ${\mathcal{O}} \colon {\mathsf{KHaus}}\to{\mathsf{KRFrm}}$ which associates with each compact Hausdorff space $X$ the compact regular frame ${\mathcal{O}}(X)$ of open subsets of $X$, and with each continuous map $f\colon X\to Y$ the frame homomorphism $f^{-1} \colon {\mathcal{O}}(Y)\to{\mathcal{O}}(X)$. De Vries duality is established by working with the contravariant functor ${\mathcal{RO}}\colon {\mathsf{KHaus}}\to{\mathsf{DeV}}$ which associates with each $X\in{\mathsf{KHaus}}$ the de Vries algebra $({\mathcal{RO}}(X),\prec)$ of regular open subsets of $X$, where $U\prec V$ iff ${\mathsf{cl}}(U)\subseteq V$, and with each continuous map $f\colon X\to Y$ the de Vries morphism ${\mathcal{RO}}(f)\colon {\mathcal{RO}}(Y)\to{\mathcal{RO}}(X)$ given by ${\mathcal{RO}}(f)(V)={\mathsf{int}}({\mathsf{cl}} f^{-1}[V])$ for each $V\in{\mathcal{RO}}(Y)$.

As a consequence of Isbell and de Vries dualities, ${\mathsf{KRFrm}}$ is equivalent to ${\mathsf{DeV}}$. This equivalence can be obtained directly, without first passing to ${\mathsf{KHaus}}$ \cite{Bez12}. We thus arrive at the following diagram, where the horizontal arrow represents an equivalence and the slanted arrows with the letter $d$ on top represent dual equivalences.
\begin{figure}[!h]
\[
\begin{tikzcd}
 & {\mathsf{KHaus}} \arrow[dl, leftrightarrow, "d"'] \arrow[dr, leftrightarrow, "d"] & \\
{\mathsf{KRFrm}} \arrow[rr, leftrightarrow] & & {\mathsf{DeV}}
\end{tikzcd}
\]
\end{figure}

Several authors have considered generalizations of ${\mathsf{KHaus}}$ where functions are replaced by relations. A relation $R$ between two compact Hausdorff spaces $X$ and $Y$ is {\em closed} if $R$ is a closed subset of $X\times Y$ and it is {\em continuous} if in addition the $R$-preimage of each open subset of $Y$ is open in $X$. A function between compact Hausdorff spaces is closed iff it is continuous. But for relations this results in two different categories $\mathsf{KHaus}^\mathsf{R}$ and $\mathsf{KHaus}^\mathsf{C}$. In the former, morphisms are closed relations; and in the latter, they are continuous relations. Clearly ${\mathsf{KHaus}}$ is a wide subcategory of $\mathsf{KHaus}^\mathsf{C}$, which in turn is a wide subcategory of $\mathsf{KHaus}^\mathsf{R}$.

In \cite{BezhanishviliGabelaiaEtAl2019} ${\mathsf{KRFrm}}$ was generalized to ${\mathsf{KRFrm^C}}$, ${\mathsf{DeV}}$ to $\mathsf{DeV^C}$, and it was shown that the commutative diagram above generalizes to the following commutative diagram.
\begin{figure}[!h]
\[
\begin{tikzcd}
 & \mathsf{KHaus}^\mathsf{C} \arrow[dl, leftrightarrow, "d"'] \arrow[dr, leftrightarrow, "d"] & \\
{\mathsf{KRFrm^C}} \arrow[rr, leftrightarrow] & & \mathsf{DeV^C}
\end{tikzcd}
\]
\end{figure}

On the other hand, in \cite{Tow96, JKM01} ${\mathsf{KRFrm}}$ was generalized to ${\mathsf{KRFrm^P}}$, where morphisms are preframe homomorphisms (that is, they preserve finite meets and directed joins), and it was shown that ${\mathsf{KRFrm^P}}$ is dually equivalent to $\mathsf{KHaus}^\mathsf{R}$. In a recent paper \cite{ABC22} we introduced the category $\mathsf{DeV^S}$ whose objects are de Vries algebras and whose morphisms are compatible subordination relations. We proved that $\mathsf{DeV^S}$ is equivalent to $\mathsf{KHaus}^\mathsf{R}$ and hence dually equivalent to ${\mathsf{KRFrm^P}}$. Thus, we arrive at the following commutative diagram that generalizes the two diagrams above.
\begin{figure}[!h]
\[
\begin{tikzcd}
 & \mathsf{KHaus}^\mathsf{R} \arrow[dl, leftrightarrow, "d"'] \arrow[dr, leftrightarrow] & \\
{\mathsf{KRFrm^P}} \arrow[rr, leftrightarrow, "d"] & & \mathsf{DeV^S}
\end{tikzcd}
\]
\end{figure}

Our aim here is to give a direct choice-free proof of the duality between ${\mathsf{KRFrm^P}}$ and $\mathsf{DeV^S}$. From this we derive a direct choice-free proof of the equivalence between ${\mathsf{KRFrm^C}}$ and $\mathsf{DeV^C}$, as well as an alternative choice-free proof of the equivalence between ${\mathsf{KRFrm}}$ and ${\mathsf{DeV}}$.

Our main tool is the category $\mathsf{SubS5^S}$ of $\mathsf{S5}$-subordination algebras introduced in \cite{ABC22}. Objects of $\mathsf{SubS5^S}$ are pairs $(B,\prec)$ where $B$ is a boolean algebra and $\prec$ is a special subordination relation on it (see Section~\ref{sec: prelims} for details).
In \cite{ABC22} we used a generalization of Stone duality to closed relations and the technique of Karoubi envelopes to show that $\mathsf{SubS5^S}$ is equivalent to the category $\mathsf{StoneE}^\mathsf{R}$ whose objects are
Stone spaces equipped with a closed equivalence relation and whose morphisms are special closed relations (see Definition~\ref{def:compatible subordinations}(\ref{def:compatible subordinations:item1})). Since $\mathsf{DeV^S}$ is a full subcategory of $\mathsf{SubS5^S}$, restricting this equivalence yields an equivalence between $\mathsf{DeV^S}$ and the full subcategory $\mathsf{Gle}^\mathsf{R}$ of $\mathsf{StoneE}^\mathsf{R}$ consisting of Gleason spaces.
It turns out that these four categories are equivalent to $\mathsf{KHaus}^\mathsf{R}$. Consequently, $\mathsf{DeV^S}$ is equivalent to $\mathsf{SubS5^S}$, but the proof goes through $\mathsf{KHaus}^\mathsf{R}$ and hence uses the axiom of choice.

In this paper we generalize MacNeille completions of boolean algebras to $\mathsf{S5}$-subordination algebras and give a direct choice-free proof of the equivalence between $\mathsf{SubS5^S}$ and $\mathsf{DeV^S}$.
We also generalize ideal completions of boolean algebras to $\mathsf{S5}$-subordination algebras and give a choice-free proof that $\mathsf{SubS5^S}$ is dually equivalent to ${\mathsf{KRFrm^P}}$.
We thus arrive at the following commutative diagram.
\begin{figure}[!h]
\[
\begin{tikzcd}
 & \mathsf{SubS5^S} \arrow[dl, leftrightarrow, "d"'] \arrow[dr, leftrightarrow] & \\
{\mathsf{KRFrm^P}} \arrow[rr, leftrightarrow, "d"] & & \mathsf{DeV^S}
\end{tikzcd}
\]
\end{figure}

We also study the wide subcategories of these categories whose morphisms encode continuous relations and continuous functions between compact Hausdorff spaces.

The paper is organized as follows.
In Section~\ref{sec: prelims} we recall the existing dualities for compact Hausdorff spaces that are relevant for our purposes.
In Section~\ref{sec: id comple} we describe ideal completions of $\mathsf{S5}$-subordination algebras, which results in a functor from $\mathsf{SubS5^S}$ to ${\mathsf{KRFrm^P}}$.
In Section~\ref{sec:MacNeille} we define MacNeille completions of $\mathsf{S5}$-subordination algebras and prove that the resulting functor yields an equivalence between $\mathsf{SubS5^S}$ and $\mathsf{DeV^S}$. We then use this result to show that the ideal completion functor from $\mathsf{SubS5^S}$ to ${\mathsf{KRFrm^P}}$ is a dual equivalence.
In Section~\ref{sec: dually} we give dual descriptions of the ideal and MacNeille completions of $\mathsf{S5}$-subordination algebras.
In Section~\ref{sec: cont subs} we study the wide subcategories of these categories whose morphisms encode continuous relations between compact Hausdorff spaces. Finally, in Section~\ref{sec:functional} we further restrict our attention to the morphisms that encode continuous functions between compact Hausdorff spaces.

\section{Preliminaries} \label{sec: prelims}

In this section we briefly recall Isbell duality, de Vries duality, and their generalizations.
We start by recalling some basic definitions from pointfree topology (see, e.g., \cite{PP12}). A {\em frame} or {\em locale} is a complete lattice $L$ satisfying the join-infinite distributive law
\[
a\wedge\bigvee S=\bigvee\{ a\wedge s \mid s\in S \}.
\]
Each $a\in L$ has the {\em pseudocomplement} given by $a^*=\bigvee\{ x\in L \mid a\wedge x=0 \}$. We say that $a$ is {\em compact} if $a\le \bigvee S$ implies $a\le \bigvee T$ for some finite $T\subseteq S$, and that $a$ is {\em well-inside} $b$ (written $a\prec b$) if $a^*\vee b=1$. A frame $L$ is {\em compact} if $1$ is compact and it is {\em regular} if $a=\bigvee\{ x\in L \mid x\prec a\}$ for each $a\in L$.

A {\em frame homomorphism} between two frames is a map
that preserves arbitrary joins and finite meets. Let ${\mathsf{KRFrm}}$ be the category of compact regular frames and frame homomorphisms.

\begin{theorem} [Isbell duality]
	${\mathsf{KRFrm}}$ is dually equivalent to ${\mathsf{KHaus}}$.
\end{theorem}

A \emph{preframe homomorphism} between two frames is a map that preserves directed joins and finite meets.
We let ${\mathsf{KRFrm^P}}$ be the category of compact regular frames and preframe homomorphisms. Clearly ${\mathsf{KRFrm}}$ is a wide subcategory of ${\mathsf{KRFrm^P}}$.

We recall that a relation $R\subseteq X\times Y$ between compact Hausdorff spaces is {\em closed} if $R$ is a closed subset of $X\times Y$. As usual, for $x\in X$ and $y\in Y$, we write
\[
R[x]=\{y\in Y\mid xRy\} \quad \mbox{and} \quad R^{-1}[y]=\{x\in X\mid xRy\}.
\]
Also, for $F\subseteq X$ and $G\subseteq Y$, we write
\[
R[F]=\bigcup\{ R[x] \mid x\in F\} \quad \mbox{and} \quad R^{-1}[G]=\bigcup \{ R^{-1}[y] \mid y\in G\}.
\]
Then $R$ is closed iff $R[F]$ is closed for each closed $F\subseteq X$ and $R^{-1}[G]$ is closed for each closed $G\subseteq Y$ (see, e.g., \cite[Lem.~3.2]{BezhanishviliGabelaiaEtAl2019}). We let $\mathsf{KHaus}^\mathsf{R}$ be the category of compact Hausdorff spaces and closed relations, where identities are identity relations and composition is the relational composition. We recall that for two relations $R_1 \subseteq X_1\times X_2$ and $R_2\subseteq X_2\times X_3$ the relation composition $R_2 \circ R_1 \subseteq X_1 \times X_3$ is defined by
\[
x_1 \mathrel{(R_2 \circ R_1)} x_3 \iff \exists x_2 \in X_2 : x_1 \mathrel{R}_1 x_2\text{ and }x_2 \mathrel{R}_2 x_3.
\]
The following theorem generalizes Isbell duality:

\begin{theorem} [\cite{Tow96, JKM01}] \label{thm:isbell-gen}
${\mathsf{KRFrm^P}}$ is dually equivalent to $\mathsf{KHaus}^\mathsf{R}$.
\end{theorem}

A closed relation $R\subseteq X\times Y$ between compact Hausdorff spaces is {\em continuous} if $V$ open in $Y$ implies $R^{-1}[V]$ is open in $X$. Let $\mathsf{KHaus}^\mathsf{C}$ be the wide subcategory of $\mathsf{KHaus}^\mathsf{R}$ consisting of continuous relations.

In \cite[Def.~4.3]{BezhanishviliGabelaiaEtAl2019}, motivated by Johnstone's construction of the Vietoris frame of a compact regular frame \cite[Sec.~III.4]{Joh82}, a preframe homomorphism $\Box \colon L \to M$ between compact regular frames is called {\em continuous} or \emph{$\mathsf{c}$-morphism} if there is a join-preserving $\Diamond \colon L \to M$ such that
\[
\Box(a \vee b) \le \Box a \vee \Diamond b \quad \mbox{and} \quad \Box a \wedge \Diamond b \le \Diamond(a \wedge b).
\]
Let ${\mathsf{KRFrm^C}}$ be the wide subcategory of ${\mathsf{KRFrm^P}}$ consisting of $\c$-morphisms. Theorem~\ref{thm:isbell-gen} then restricts to the following generalization of Isbell duality:

\begin{theorem}[{\cite[Thm.~4.8]{BezhanishviliGabelaiaEtAl2019}}]
	${\mathsf{KRFrm^C}}$ is dually equivalent to $\mathsf{KHaus}^\mathsf{C}$.
\end{theorem}

Letting $\Diamond = \Box$, we can identify ${\mathsf{KRFrm}}$ with a wide subcategory of ${\mathsf{KRFrm^C}}$. Thus, we arrive at the following diagram, where the hook arrows represent being a wide subcategory.
\[
\begin{tikzcd}[column sep=4em]
{\mathsf{KRFrm^P}} \arrow[r, leftrightarrow] & \mathsf{KHaus}^\mathsf{R} \\
{\mathsf{KRFrm^C}} \arrow[u, hookrightarrow] \arrow[r, leftrightarrow] & \mathsf{KHaus}^\mathsf{C} \arrow[u, hookrightarrow] \\
{\mathsf{KRFrm}} \arrow[u, hookrightarrow] \arrow[r, leftrightarrow] & {\mathsf{KHaus}} \arrow[u, hookrightarrow]
\end{tikzcd}
\]

Let $B$ be a boolean algebra. A binary relation $S$ on $B$ is a \emph{subordination} if $S$ satisfies the following conditions for all $a,b,c,d\in B$:
\begin{enumerate}[label = (S\arabic*), ref = S\arabic*]
\item \label{S1} $0 \mathrel{S} 0$ and $1 \mathrel{S} 1$;
\item \label{S2} $a,b \mathrel{S} c$ implies $(a\vee b) \mathrel{S} c$;
\item \label{S3} $a \mathrel{S} c,d$ implies $a \mathrel{S} (c\wedge d)$;
\item \label{S4} $a\le b \mathrel{S} c\le d$ implies $a \mathrel{S} d$;
\end{enumerate}

Subordination relations were introduced in~\cite{BBSV17} as a counterpart of quasi-modal operators~\cite{Celani2001} and precontact relations~\cite{DV06,DuentschVakarelov2007}. Subordinations on $B$ correspond to closed relations $R$ on the Stone space of $B$.
Whether $R$ is reflexive, symmetric, or transitive is characterized by the axioms:

\begin{enumerate}[label = (S\arabic*), ref = S\arabic*]
\setcounter{enumi}{4}
\item \label{S5} $a \mathrel{S} b$ implies $a \le b$;
\item \label{S6} $a \mathrel{S} b$ implies $\neg b \mathrel{S} \neg a$;
\item \label{S7} $a \mathrel{S} b$ implies there is $c \in B$ with $a \mathrel{S} c$ and $c \mathrel{S} b$.
\end{enumerate}

Following the modal logic nomenclature, the pairs $(B,S)$ where $S$ satisfies \eqref{S1}--\eqref{S7} were called \emph{$\mathsf{S5}$-subordination} algebras in \cite{ABC22}.

\begin{definition} \cite[Def.~1.1.1]{deV62}
	An $\mathsf{S5}$-subordination algebra $(B, S)$ is a \emph{compingent algebra} if $S$ satisfies the following axiom:
	\begin{enumerate}[label = (S\arabic*), ref = S\arabic*]
		\setcounter{enumi}{7}
		\item \label{S8} If $a \neq 0$, then there is $b \neq 0$ with $b \mathrel{S} a$.
	\end{enumerate}
\end{definition}

A relation $S$ on a boolean algebra $B$ satisfying \eqref{S1}--\eqref{S8} is called a \emph{de Vries proximity} on $B$ and is usually denoted by $\prec$.
When a compingent algebra is complete as a boolean algebra, it is called a \emph{de Vries algebra} (see \cite{Bez10}).

A {\em de Vries morphism} between de Vries algebras is a map $f\colon A \to B$ satisfying the following conditions:
	\begin{enumerate}[label = (M\arabic*), ref = M\arabic*]
		\item\label{M1} $f(0) = 0$;
		\item\label{M2} $f(a \land b) = f(a) \land f(b)$;
		\item\label{M3} $a \prec b$ implies $\lnot f(\lnot a) \prec f(b)$;
		\item\label{M4} $f(a) = \bigvee \{f(b) \mid b \prec a\}$.
	\end{enumerate}
	The composition of two de Vries morphisms $f \colon A \to B$ and $g \colon B \to C$ is the de Vries morphism $g * f \colon A \to C$ given by
	\[
		(g * f)(a) = \bigvee \{ gf(b) \mid b \prec a \}
	\]
	for each $a\in A$. Let ${\mathsf{DeV}}$ be the category of de Vries algebras and de Vries morphisms, where identity morphisms are identity functions and  composition is defined as above.

\begin{theorem} [de Vries duality]
	${\mathsf{DeV}}$ is dually equivalent to ${\mathsf{KHaus}}$.
\end{theorem}

In \cite{BezhanishviliGabelaiaEtAl2019} de Vries duality was generalized to a duality for $\mathsf{KHaus}^\mathsf{C}$. For this, the notion of a de Vries additive map from \cite{BBH15} was utilized. We will instead work with the equivalent notion of a de Vries multiplicative map.

\begin{definition}
A map $\Box \colon A\to B$ between de Vries algebras is {\em de Vries multiplicative} if $\Box 1 = 1$ and for all $a_1,a_2,b_1,b_2\in A$, we have:
\[
a_1 \prec a_2 \mbox{ and } b_1 \prec b_2 \mbox{ imply } \Box a_1 \wedge \Box b_1 \prec \Box(a_2 \wedge b_2).
\]
We call $\Box$ {\em lower continuous} if in addition
\[
\Box a = \bigvee \{ \Box b \mid b \prec a\}
\]
for each $a\in A$. The composition of two such maps $\Box_1$ and $\Box_2$ is given by
	\[
		(\Box_2 * \Box_1) a = \bigvee \{ \Box_2\Box_1 b \mid b \prec a \}.
	\]
Let $\mathsf{DeV^C}$ be the category of de Vries algebras and lower continuous de Vries multiplicative maps, where identity morphisms are identity functions and  composition is defined as above.
\end{definition}

\begin{remark}\label{rem:box diamond upper lower}
The results of \cite{BezhanishviliGabelaiaEtAl2019} are stated using de Vries additive maps $\Diamond$ that are lower continuous. But in our setting it is preferable to work with lower continuous de Vries multiplicative maps $\Box$.
As observed in~\cite[Rem.~4.11]{BezhanishviliGabelaiaEtAl2019}, working with lower continuous de Vries additive maps is equivalent to working with de Vries multiplicative maps that are upper continuous, i.e.\ maps $\Box$ that satisfy $\Box a = \bigwedge \{ \Box b \mid a \prec b\}$. Analogously, working with de Vries multiplicative lower continuous maps is equivalent to working with de Vries additive maps that are upper continuous.
It is shown in \cite[Cor.~4.24]{BBH15} that the category of de Vries algebras equipped with de Vries additive upper continuous maps is equivalent to the category of de Vries algebras equipped with de Vries additive lower continuous maps. Similarly, one can show that $\mathsf{DeV^C}$ is equivalent to the category of de Vries algebras and upper continuous de Vries multiplicative maps, and hence to the category of de Vries algebras and lower continuous de Vries additive maps. Thus, the results of~\cite{BezhanishviliGabelaiaEtAl2019} apply to our setting.
\end{remark}

\begin{theorem}[{\cite[Thm.~4.14]{BezhanishviliGabelaiaEtAl2019}}]
$\mathsf{DeV^C}$ is dually equivalent to $\mathsf{KHaus}^\mathsf{C}$.
\end{theorem}

In \cite{BezhanishviliGabelaiaEtAl2019} obtaining a de Vries like duality for $\mathsf{KHaus}^\mathsf{R}$ was left open. This question was resolved in \cite{ABC22} by working with special subordination relations between de Vries algebras.

\begin{definition}\label{def:compatible subordinations}
\mbox{}\begin{enumerate}
\item\label{def:compatible subordinations:item1} Let $(B_1,S_1)$ and $(B_2,S_2)$ be $\mathsf{S5}$-subordination algebras. We call a subordination $T\subseteq B_1\times B_2$ {\em compatible} if $S_2\circ T=T=T\circ S_1$.

\item\label{def:compatible subordinations:item2} Let $\mathsf{SubS5^S}$ be the category of $\mathsf{S5}$-subordination algebras and compatible subordinations, where the composition of morphisms is the usual composition of relations, and the identity morphism on an $\mathsf{S5}$-subordination algebra $(B,S)$ is the relation $S$.
\item\label{def:compatible subordinations:item3} Let $\mathsf{Comp^S}$ be the full subcategory of $\mathsf{SubS5^S}$ consisting of compingent algebras, and $\mathsf{DeV^S}$ the full subcategory of $\mathsf{Comp^S}$ consisting of de Vries algebras.
\end{enumerate}
\end{definition}

To connect $\mathsf{KHaus}^\mathsf{R}$ with $\mathsf{SubS5^S}$, it is convenient to first obtain a Stone-like representation of $\mathsf{S5}$-subordination algebras.

\begin{definition}

\mbox{}\begin{enumerate}
		\item
		An \emph{$\mathsf{S5}$-subordination space} is a pair $(X, E)$ where $X$ is a Stone space and $E$ is a closed equivalence relation on $X$.
		We let $\mathsf{StoneE}^\mathsf{R}$ be the category whose objects are $\mathsf{S5}$-subordination spaces and whose morphisms are closed relations $R$ between $(X,E_X)$ and $(Y,E_Y)$
		such that $R \circ E_X = R = E_Y \circ R$.

		\item	A \emph{Gleason space} is an $\mathsf{S5}$-subordination space $(X,E)$ such that $X$ is extremally disconnected and $E$ is \emph{irreducible} (i.e., if $F$ is a proper closed subset of $X$, then so is $E[F]$).
		We let $\mathsf{Gle}^\mathsf{R}$
		be the full subcategory of $\mathsf{StoneE}^\mathsf{R}$ whose objects are Gleason spaces.
	\end{enumerate}
\end{definition}

\begin{theorem} [{\cite[Thm.~6.15]{ABC22}}] \label{thm:equiv-ABC}
	The categories $\mathsf{KHaus}^\mathsf{R}$, $\mathsf{StoneE}^\mathsf{R}$, $\mathsf{Gle}^\mathsf{R}$, $\mathsf{SubS5^S}$, $\mathsf{Comp^S}$, and $\mathsf{DeV^S}$ are equivalent.
\end{theorem}

To make the paper self-contained, we briefly describe the functors yielding some of the equivalences of Theorem~\ref{thm:equiv-ABC}.

\begin{remark}\label{rem:functors equivalences}
\mbox{}
\begin{enumerate}
	\item \label{i:functor-Q}
	The functor $\mathcal{Q} \colon \mathsf{StoneE}^\mathsf{R} \to \mathsf{KHaus}^\mathsf{R}$ maps an object $(X, E)$ to the quotient space $X/E$, and a morphism $R \colon (X, E_X) \to (Y, E_Y)$ to the morphism $\mathcal{Q}(R) \colon \mathcal{Q}(X,E_X) \to \mathcal{Q}(Y,E_Y)$
	given by $[x]_{E_X} \mathrel{\mathcal{Q}(R)} [y]_{E_Y}$ iff $x \mathrel{R} y$.
	\item \label{i:functor-G}
	A quasi-inverse of $\mathcal{Q}$ is given by the Gleason cover functor ${\mathcal{G}} \colon \mathsf{KHaus}^\mathsf{R} \to \mathsf{StoneE}^\mathsf{R}$ which associates to each compact Hausdorff space $X$ the pair ${\mathcal{G}}(X)=(\widehat{X}, E)$ where $g_X \colon \widehat{X} \to X$ is the Gleason cover of $X$ and $x \mathrel{E} y$ iff $g_X(x)=g_X(y)$.
	It also maps a closed relation $R \colon X \to Y$ to the relation
	${\mathcal{G}}(R) \colon {\mathcal{G}}(X) \to {\mathcal{G}}(Y)$ given by $x \mathrel{{\mathcal{G}}(R)} y$ iff $g_{X}(x) \mathrel{R} g_{Y}(y)$.
	\item The functor $\mathcal{G}$ is also a quasi-inverse of the restriction of the functor $\mathcal{Q}$ to $\mathsf{Gle}^\mathsf{R}$.
	\item\label{i:GleR StoneER equivalence} The inclusion of $\mathsf{Gle}^\mathsf{R}$ into $\mathsf{StoneE}^\mathsf{R}$ is an equivalence whose quasi-inverse is the composition ${\mathcal{G}} \circ \mathcal{Q}$.
	\item \label{i:functor-Clop}
	The functor ${\mathsf{Clop}} \colon \mathsf{StoneE}^\mathsf{R} \to \mathsf{SubS5^S}$ maps an object $(X, E)$ to
	$({\mathsf{Clop}}(X), S)$, where ${\mathsf{Clop}}(X)$ is the boolean algebra of clopen subsets of $X$ and $S_E$ is the binary relation on ${\mathsf{Clop}}(X)$ given by $U \mathrel{S}_E V$ iff $E[U] \subseteq V$. Also, ${\mathsf{Clop}}$ maps a morphism $R \colon (X, E_X) \to (Y, E_Y)$ to the compatible subordination relation $S_R \colon {\mathsf{Clop}}(X) \to {\mathsf{Clop}}(Y)$ given by $U \mathrel{S}_R V$ iff $R[U] \subseteq V$.
	\item \label{i:functor-Ult}
	A quasi-inverse of ${\mathsf{Clop}}$ is given by the ultrafilter functor ${\mathsf{Ult}} \colon \mathsf{SubS5^S} \to \mathsf{StoneE}^\mathsf{R}$ which associates to each
	object $(B,S)$ the pair ${\mathsf{Ult}}(B,S)=(X,R_S)$ where $X$ is the Stone space of ultrafilters of $B$ and $x \mathrel{R}_S y$ iff $S[x] \subseteq y$. We call $(X,R_S)$ the \emph{$\mathsf{S5}$-subordination space} of $(B,S)$. A morphism $T \colon (B_1,S_1) \to (B_2,S_2)$ is mapped by ${\mathsf{Ult}}$ to the morphism $R_T \colon {\mathsf{Ult}}(B_1,S_1) \to {\mathsf{Ult}}(B_2,S_2)$ given by $x \mathrel{R}_T y$ iff $T[x] \subseteq y$.
	\item The functor ${\mathsf{Clop}}$ is also a quasi-inverse of the restriction of ${\mathsf{Ult}}$ to $\mathsf{Comp^S}$ and $\mathsf{DeV^S}$.
\end{enumerate}
\end{remark}

It follows from Theorems~\ref{thm:isbell-gen} and~\ref{thm:equiv-ABC} that $\mathsf{SubS5^S}$ is dually equivalent to ${\mathsf{KRFrm^P}}$ and equivalent to $\mathsf{DeV^S}$. We give direct choice-free proofs of these results by generalizing ideal and MacNeille completions of boolean algebras to the setting of $\mathsf{S5}$-subordination algebras.
We also fill in the empty boxes of the following diagram and show that it commutes up to natural isomorphism. The unlabeled horizontal arrows in the diagram represent equivalences of categories while the ones labeled with the letter d represent dual equivalences. The vertical arrows are inclusions of wide subcategories.
Because of the lack of space, the equivalences and dual equivalences involving $\mathsf{Comp^S}$ are left out.

\begin{figure}[h]
\[
\begin{tikzcd}[column sep=0.90cm]
\mathsf{SubS5^S} \arrow[r, leftrightarrow] & \mathsf{DeV^S} \arrow[rr, leftrightarrow, "d"] & & {\mathsf{KRFrm^P}} \arrow[r, leftrightarrow, "d"] & \mathsf{KHaus}^\mathsf{R} \arrow[r, leftrightarrow] & \mathsf{StoneE}^\mathsf{R} \arrow[r, leftrightarrow] & \mathsf{Gle}^\mathsf{R} \\
\boxed{\phantom{{\mathsf{DeV}}}} \arrow[u, hookrightarrow] \arrow[r, leftrightarrow] & \boxed{\phantom{{\mathsf{DeV}}}} \arrow[u, hookrightarrow] \arrow[r, leftrightarrow, "d"] & \mathsf{DeV^C} \arrow[r, leftrightarrow] & {\mathsf{KRFrm^C}} \arrow[u, hookrightarrow] \arrow[r, leftrightarrow, "d"] & \mathsf{KHaus}^\mathsf{C} \arrow[u, hookrightarrow] \arrow[r, leftrightarrow] & \boxed{\phantom{{\mathsf{DeV}}}} \arrow[u, hookrightarrow] \arrow[r, leftrightarrow] & \boxed{\phantom{{\mathsf{DeV}}}} \arrow[u, hookrightarrow] \\
\boxed{\phantom{{\mathsf{DeV}}}} \arrow[u, hookrightarrow] \arrow[r, leftrightarrow] & \boxed{\phantom{{\mathsf{DeV}}}} \arrow[u, hookrightarrow] \arrow[r, leftrightarrow, "d"] & {\mathsf{DeV}} \arrow[u, hookrightarrow] \arrow[r, leftrightarrow] & {\mathsf{KRFrm}} \arrow[u, hookrightarrow] \arrow[r, leftrightarrow, "d"] & {\mathsf{KHaus}} \arrow[u, hookrightarrow] \arrow[r, leftrightarrow] & \boxed{\phantom{{\mathsf{DeV}}}} \arrow[u, hookrightarrow] \arrow[r, leftrightarrow] & \boxed{\phantom{{\mathsf{DeV}}}} \arrow[u, hookrightarrow]
\end{tikzcd}
\]
\end{figure}

\section{Ideal completions of $\mathsf{S5}$-subordination algebras}\label{sec: id comple}

For a boolean algebra $B$, let $\mathcal I(B)$ be the set of ideals of $B$ ordered by inclusion. It is well known that $\mathcal I(B)$ is a frame, where $I\wedge J=I\cap J$ and $\bigvee I_\alpha$ is the ideal generated by $\bigcup I_\alpha$. Moreover, the compact elements of $\mathcal I(B)$ are the principal ideals. This in particular implies that $\mathcal I(B)$ is compact and regular.\footnote{The frame $\mathcal I(B)$ is even zero-dimensional because every element in $\mathcal I(B)$ is a join of complemented elements (see, e.g., \cite[p.~81]{Joh82}).}
We show that similar results hold for $\mathsf{S5}$-subordination algebras. For this we introduce the concept of a subordination ideal.

\begin{definition}
	Let $\mathbf B=(B,S)$ be an $\mathsf{S5}$-subordination algebra. We call an ideal $I$ of $B$ a {\em subordination ideal}, or {\em S-ideal} for short, if $a\in I$ implies $a\mathrel{S} b$ for some $b\in I$. Let ${\mathcal{SI}}(\mathbf B)$ be the set of S-ideals of $\mathbf{B}$ ordered by inclusion.
\end{definition}

\begin{remark}\label{rem:S-ideal}
An ideal $I$ is an S-ideal iff $I \subseteq S^{-1}[I]$. By \eqref{S5}, this condition is equivalent to $I=S^{-1}[I]$.
\end{remark}

\begin{lemma} {\cite[Lem.~3.3(1)]{ABC22}} \label{lem: K4-sub}
	Let $\mathbf B$ be an $\mathsf{S5}$-subordination algebra. If $I$ is an ideal of $B$, then $S^{-1}[I]$ is an S-ideal of $\mathbf B$.
\end{lemma}

\begin{remark}\label{rem: S-filter}
The notion of an S-filter is dual to that of an S-ideal, and if $F$ is a filter of $B$, then $S[F]$ is an S-filter of $(B,S)$ (see \cite[Lem.~3.3(1)]{ABC22}).
\end{remark}

\begin{lemma}
	Let $\mathbf B$ be an $\mathsf{S5}$-subordination algebra.
	Then ${\mathcal{SI}}(\mathbf B)$ is a subframe of $\mathcal I(\mathbf B)$.
\end{lemma}

\begin{proof}
Since $B$ is an S-ideal, it is sufficient to show that $I,J \in {\mathcal{SI}}(\mathbf B)$ implies $I \cap J \in {\mathcal{SI}}(\mathbf B)$ and that $\{ I_\alpha \} \subseteq {\mathcal{SI}}(\mathbf B)$ implies $\bigvee I_\alpha \in {\mathcal{SI}}(\mathbf B)$.
	First suppose that $I,J \in {\mathcal{SI}}(\mathbf B)$. Then $I\cap J$ is an ideal of $B$. Let $a \in I \cap J$. Since $I$ and $J$ are S-ideals, there exist $b \in I$ and $c \in J$ such that $a \mathrel{S} b$ and $a \mathrel{S} c$. Therefore, $a \mathrel{S} (b \wedge c)$ by \eqref{S3}, and $b \wedge c \in I \cap J$. Thus, $I \cap J$ is an S-ideal.

	Next suppose that $\{ I_\alpha \} \subseteq {\mathcal{SI}}(\mathbf{B})$.
	Then $\bigvee I_\alpha$ is an ideal of $B$.
	Let $a \in \bigvee I_\alpha$, so there are $b_1, \ldots, b_n \in \bigcup I_\alpha$ such that $a \le b_1 \vee \cdots \vee b_n$. Since each $I_\alpha$ is an S-ideal, there are $c_1, \ldots, c_n \in \bigcup I_\alpha$ such that $b_i \mathrel{S} c_i$ for each $i=1, \ldots, n$. Therefore, $(b_1 \vee \cdots \vee b_n) \mathrel{S} (c_1 \vee \cdots \vee c_n)$ by \eqref{S2} and \eqref{S4}, which implies that $a \mathrel{S} (c_1 \vee \cdots \vee c_n) \in \bigvee I_\alpha$. Thus, $\bigvee I_\alpha$ is an S-ideal.
\end{proof}

Let $B$ be a boolean algebra and $X \subseteq B$. We denote by $U(X)$ the set of upper bounds of $X$, by $L(X)$ the set of lower bounds of $X$, and by $\neg X$ the set $\{ \neg x \mid x \in X \}$. It is well known that $U(X)$ is a filter, $L(X)$ is an ideal, $\neg\neg X=X$, and
$X$ is a filter iff $\neg X$ is an ideal. Moreover, $\neg U(X)=L(\neg X)$ and $\neg L(X)=U(\neg X)$.

\begin{lemma}\label{lem:operators and negations}
Let $B$ be a boolean algebra and $S$ an $\mathsf{S5}$-subordination on $B$. If $X \subseteq B$, then
\[
\neg S[X]=S^{-1}[\neg X] \quad \mbox{and} \quad \neg S^{-1}[X]=S[\neg X].
\]
\end{lemma}

\begin{proof}
	We only prove the first equality since the second is proved similarly. We have that $a \in \neg S[X]$ iff there is $x \in X$ such that $x \mathrel{S} \neg a$. By  \eqref{S6} this is equivalent to the existence of $x \in X$ such that $a \mathrel{S} \neg x$, which means that $a \in S^{-1}[\neg X]$.
\end{proof}

For the next lemma we recall that if $L$ is a frame and $a \in L$, then $a^*$ denotes the pseudocomplement of $a$.

\begin{lemma} \label{lem: pseudocomplement}
	Let $\mathbf{B}$ be an $\mathsf{S5}$-subordination algebra. If $I\in{\mathcal{SI}}(\mathbf{B})$, then $I^*=\neg S[U(I)]$.
\end{lemma}

\begin{proof}
	Let $I \in {\mathcal{SI}}(\mathbf{B})$.
	Since $U(I)$ is a filter, Remark~\ref{rem: S-filter} implies that $S[U(I)]$ is a filter. Therefore, $\neg S[U(I)]$ is an ideal. Since $S$ is an $\mathsf{S5}$-subordination, Lemma~\ref{lem:operators and negations} yields that
	\[
	S^{-1}[\neg S[U(I)]]=\neg S[S[U(I)]]
	=\neg S[U(I)].
	\]
	Thus, $\neg S[U(I)]$ is an S-ideal. To see that $\neg S[U(I)]$ is the pseudocomplement of $I$ in ${\mathcal{SI}}(\mathbf{B})$, we need to show that $I \cap \neg S[U(I)] = \{ 0 \}$ and that $I \cap J = \{ 0 \}$ implies $J \subseteq \neg S[U(I)]$ for each $J \in {\mathcal{SI}}(\mathbf{B})$.

	First suppose that $a \in I \cap \neg S[U(I)]$. Then $\lnot a \in S[U(I)] \subseteq U(I)$ by \eqref{S5}. Therefore, $a \leq \lnot a$, and hence $a = 0$.
	Next suppose that $I \cap J = \{0\}$. Then for any $x \in I$ and $y \in J$ we have $x \wedge y = 0$, so $y \le \neg x$.
	Therefore, $J \subseteq L(\neg I)$. By Lemma~\ref{lem:operators and negations},
	\[
	J=S^{-1}[J] \subseteq S^{-1}[L(\neg I)]=S^{-1}[\neg U(I)]=\neg S[U(I)].
	\]
	Thus, $I^*=\neg S[U(I)]$.
\end{proof}

\begin{lemma}\label{lem:well-inside}
	Let $\mathbf{B}$ be an $\mathsf{S5}$-subordination algebra and $I,J\in{\mathcal{SI}}(\mathbf{B})$. Then $I \prec J$ iff $U(I) \cap J \neq \varnothing$.
\end{lemma}

\begin{proof}
	By definition,
	$I \prec J$ iff $I^* \vee J=B$, which is equivalent to $\neg S[U(I)] \vee J =B$ by Lemma~\ref{lem: pseudocomplement}. This
	holds iff there are $a \in S[U(I)]$ and $b \in J$ such that $\neg a \vee b=1$. Since $B$ is a boolean algebra, $\neg a \vee b = 1$ iff $a \le b$.
	Because $S[U(I)]$ is a filter (see Remark~\ref{rem: S-filter}), the existence of $a \in S[U(I)]$ with $a \le b$ is equivalent to $b \in S[U(I)]$. Thus, $I \prec J$ iff $S[U(I)] \cap J \neq \varnothing$.
	We have that $S[U(I)] \cap J \neq \varnothing$ iff $U(I) \cap S^{-1}[J] \neq \varnothing$. Since $J$ is an S-ideal, this is equivalent to $U(I) \cap J \neq \varnothing$.
\end{proof}

\begin{proposition}\label{prop:RI compact regular}
	If $\mathbf{B}$ is an $\mathsf{S5}$-subordination algebra, then ${\mathcal{SI}}(\mathbf{B})$ is a compact regular frame.
\end{proposition}

\begin{proof}
	Since ${\mathcal{SI}}(\mathbf{B})$ is a subframe of $\mathcal I(\mathbf{B})$ and $\mathcal I(\mathbf{B})$ is compact, ${\mathcal{SI}}(\mathbf{B})$ is compact.
	To see that ${\mathcal{SI}}(\mathbf{B})$ is regular, we need to show that $J = \bigvee \{ I \in {\mathcal{SI}}(\mathbf{B}) \mid I \prec J \}$ for each $J \in {\mathcal{SI}}(\mathbf{B})$. It is sufficient to show that for each $a \in J$, there is $I \in {\mathcal{SI}}(\mathbf{B})$ such that $a \in I$ and $I \prec J$. Let $a \in J$. Since $J$ is an S-ideal, there is $b \in J$ with $a \mathrel{S} b$. Let $I=S^{-1}[b]$. Then $a \in I$ and $I$ is an S-ideal (see Lemma~\ref{lem: K4-sub}). Moreover, $b \in U(I)$ by \eqref{S5}. Therefore, since $b \in J$, we have that $U(I)\cap J\ne\varnothing$. Thus, $I \prec J$ by Lemma~\ref{lem:well-inside}.
\end{proof}

Let $\mathbf{B}_1$ and $\mathbf{B}_2$ be $\mathsf{S5}$-subordination algebras and $T \colon \mathbf{B}_1 \to \mathbf{B}_2$ a compatible subordination. We define ${\mathcal{SI}}(T) \colon {\mathcal{SI}}(\mathbf{B}_2) \to {\mathcal{SI}}(\mathbf{B}_1)$ by setting ${\mathcal{SI}}(T)(I)=T^{-1}[I]$ for each S-ideal $I$ of $\mathbf{B}_2$.

\begin{proposition}\label{prop:SI(T) preframe hom}
If $T$ is a compatible subordination, then ${\mathcal{SI}}(T)$ is a preframe homomorphism.
\end{proposition}

\begin{proof}
Let $T$ be a compatible subordination from $\mathbf{B}_1=(B_1,S_1)$ to $\mathbf{B}_2=(B_2,S_2)$. If $I \in {\mathcal{SI}}(\mathbf{B}_2)$, then $T^{-1}[I]$ is an ideal by Lemma~\ref{lem: K4-sub}. Since $T$ is compatible, $S_1^{-1} T^{-1}[I]= (T \circ S_1)^{-1}[I]=T^{-1}[I]$, and hence $T^{-1}[I]$ is an S-ideal by Remark~\ref{rem:S-ideal}. Thus, ${\mathcal{SI}}(T)$ is well defined.
To show that ${\mathcal{SI}}(T)$ is a preframe homomorphism, we need to prove that it preserves directed joins and finite meets. That it preserves directed joins is straightforward because directed joins are set-theoretic unions in ${\mathcal{I}}(\mathbf{B}_1)$ and ${\mathcal{I}}(\mathbf{B}_2)$, and hence also in their subframes ${\mathcal{SI}}(\mathbf{B}_1)$ and ${\mathcal{SI}}(\mathbf{B}_2)$.
Moreover, we have that $T^{-1}[B_2]=B_1$ because $a \mathrel{T} 1$ for each $a \in B_1$. Thus, it remains to show that ${\mathcal{SI}}(T)$ preserves binary meets. Let $I,J \in {\mathcal{SI}}(\mathbf{B}_2)$. Clearly $T^{-1}[I \cap J] \subseteq T^{-1}[I] \cap T^{-1}[J]$. For the other inclusion, let $a \in T^{-1}[I] \cap T^{-1}[J]$. Then there are $b \in I$, $c \in J$ such that $a \mathrel{T} b$ and $a \mathrel{T} c$. Therefore, $a \mathrel{T} (b \wedge c) \in I \cap J$ by \eqref{S3}, and hence $a \in T^{-1}[I \cap J]$.
\end{proof}

It is straightforward to show that ${\mathcal{SI}}$ preserves identities and reverses compositions. Thus, we obtain the following:

\begin{theorem} \label{thm: RI contravariant}
${\mathcal{SI}}\colon \mathsf{SubS5^S} \to {\mathsf{KRFrm^P}}$ is a well-defined contravariant functor.
\end{theorem}

In the next section we will show that ${\mathcal{SI}}$ is a dual equivalence.

\section{MacNeille completions of $\mathsf{S5}$-subordination algebras}\label{sec:MacNeille}

In \cite{ABC22} we showed that the categories $\mathsf{SubS5^S}$, $\mathsf{Comp^S}$, and $\mathsf{DeV^S}$ are equivalent. This was done by observing that each of these categories is equivalent to $\mathsf{KHaus}^\mathsf{R}$. In this section we show that the equivalence can be obtained directly by generalizing the theory of MacNeille completions of boolean algebras to $\mathsf{S5}$-subordination algebras.

For a frame $L$, we recall (see, e.g., \cite{BP96}) that the {\em booleanization} of $L$ is
\[
{\mathfrak{B}} L=\{ a\in L \mid a=a^{**} \},
\]
and that $({\mathfrak{B}} L,\sqcap,\bigsqcup)$ is a boolean frame (complete boolean algebra), where
\[
a\sqcap b=a\wedge b \quad \mbox{and} \quad \bigsqcup S = \left(\bigvee S\right)^{**}.
\]
If $L$ is compact regular, then $({\mathfrak{B}} L,\prec)$ is a de Vries algebra, where $\prec$ is the restriction of the well-inside relation on $L$ to ${\mathfrak{B}} L$. As was shown in \cite{Bez12}, this correspondence extends to a covariant functor ${\mathfrak{B}}\colon{\mathsf{KRFrm}}\to{\mathsf{DeV}}$ which is an equivalence. In the more general setting of ${\mathsf{KRFrm^P}}$ and $\mathsf{DeV^S}$, this correspondence extends to a contravariant functor as follows.

Let $\Box \colon L \to M$ be a preframe homomorphism. Define the relation ${\mathfrak{B}}(\Box) \colon {\mathfrak{B}} M \to {\mathfrak{B}} L$ by
\[
b \mathrel{{\mathfrak{B}}(\Box)} a \mbox{ iff } b \prec \Box a.
\]

\begin{lemma}\label{lem:boolf compatible}
If $\Box \colon L \to M$ is a preframe homomorphism, then ${\mathfrak{B}}(\Box) \colon {\mathfrak{B}} M \to {\mathfrak{B}} L$ is a compatible subordination relation.
\end{lemma}

\begin{proof}
Let $T = {\mathfrak{B}}(\Box)$. It is straightforward to check that $T$ is a subordination. We only verify \eqref{S3}. Suppose $b \mathrel{T} a, c$. Then $b \prec \Box a$ and $b \prec \Box c$. Since $\Box$ is a preframe homomorphism and $\prec$ is a subordination, we have $b \prec \Box a \wedge \Box c = \Box(a \wedge c)$. Thus, $T$ satisfies \eqref{S3}. We next prove that $T$ is compatible. Let $a \in {\mathfrak{B}} L$ and $b \in {\mathfrak{B}} M$. Since ${\mathfrak{B}} M$ is a de Vries algebra, it is easy to see that $b \mathrel{T} a$ iff there is $d \in {\mathfrak{B}} M$ such that $b \prec d \mathrel{T} a$. It remains to show that $b \mathrel{T} a$ iff there is $c \in {\mathfrak{B}} L$ such that $b \mathrel{T} c \prec a$. For the right-to-left implication, we have that $c \prec a$ implies $c \le a$, and hence $\Box c \le \Box a$ because $\Box$ is order-preserving. Since $b \prec \Box c$, it follows that $b \prec \Box a$, and so $b \mathrel{T} a$. For the left-to-right implication, since $L$ is a compact regular frame,
$a$ is the directed join of $\{c \in {\mathfrak{B}} L \mid c \prec a \}$. Therefore, since $\Box$ preserves directed joins, $\Box a = \bigvee \{ \Box c \mid c \in {\mathfrak{B}} L, \ c \prec a \}$.
Thus, from $b \prec \Box a$,
using compactness, we find $c \in {\mathfrak{B}} L$ such that $c \prec a$ and $b \prec \Box c$.
\end{proof}

We thus define ${\mathfrak{B}} \colon {\mathsf{KRFrm^P}} \to \mathsf{DeV^S}$ by sending each compact regular frame $L$ to $({\mathfrak{B}} L,\prec)$ and each preframe homomorphism $\Box\colon L\to M$ to ${\mathfrak{B}}(\Box)$.

\begin{proposition} \label{prop: B contravariant}
${\mathfrak{B}} \colon {\mathsf{KRFrm^P}} \to \mathsf{DeV^S}$ is a contravariant functor.
\end{proposition}

\begin{proof}
That ${\mathfrak{B}}$ is well defined on objects follows from \cite[Lem.~3.1]{Bez12} and that it is well defined on morphisms from Lemma~\ref{lem:boolf compatible}.
Let $L$ be a compact regular frame. If $\Box$ is the identity on $L$, then ${\mathfrak{B}}(\Box)$ coincides with $\prec$ which is the identity on $(\mathfrak B L,\prec)$.
Let $\Box_1 \colon L \to M$ and $\Box_2 \colon M \to N$ be two preframe homomorphisms between compact regular frames.
We show that ${\mathfrak{B}}(\Box_2 \circ \Box_1) = {\mathfrak{B}}(\Box_1) \circ {\mathfrak{B}}(\Box_2)$. Let $T_1={\mathfrak{B}}(\Box_1)$ and $T_2={\mathfrak{B}}(\Box_2)$.
For $a \in {\mathfrak{B}} L$ and $c \in {\mathfrak{B}} N$, if $c \mathrel{(T_1 \circ T_2)} a$, then there is $b \in {\mathfrak{B}} M$ such that $c \mathrel{T}_2 b$ and $b \mathrel{T}_1 a$.
Thus, $c \prec \Box_2 b$ and $b \prec \Box_1 a$.
Since $b \prec \Box_1 a$ and $\Box_2$ is order-preserving, we have $\Box_2 b \le \Box_2\Box_1 a$.
Therefore, $c \prec \Box_2\Box_1 a$ which means that $c \mathrel{{\mathfrak{B}}(\Box_2 \circ \Box_1)} a$.
Suppose next that $c \mathrel{{\mathfrak{B}}(\Box_2 \circ \Box_1)} a$.
Therefore, $c \prec \Box_2 \Box_1 a$, and hence $c \mathrel{T}_2 \Box_1 a$.
Since $T_2$ is a compatible subordination, there is $b \in {\mathfrak{B}} M$ such that $c \mathrel{T}_2 b$ and $b \prec \Box_1 a$.
Thus, $c \mathrel{T}_2 b$ and $b \mathrel{T}_1 a$ which means that $c \mathrel{(T_1 \circ T_2)} a$.
\end{proof}

\begin{definition}
Let ${\mathcal{NI}} = {\mathfrak{B}} \circ {\mathcal{SI}}$.
\[
\begin{tikzcd}
\mathsf{SubS5^S} \arrow[r, "{\mathcal{SI}}"'] \arrow[rr, bend left=25, "{\mathcal{NI}}"] &  {\mathsf{KRFrm^P}} \arrow[r, "{\mathfrak{B}}"'] & \mathsf{DeV^S}
\end{tikzcd}
\]
\end{definition}

By Theorem~\ref{thm: RI contravariant} ${\mathcal{SI}} \colon \mathsf{SubS5^S} \to {\mathsf{KRFrm^P}}$ is a contravariant functor, and by Proposition~\ref{prop: B contravariant} ${\mathfrak{B}} \colon {\mathsf{KRFrm^P}} \to \mathsf{DeV^S}$ is a contravariant functor. Thus, ${\mathcal{NI}} \colon \mathsf{SubS5^S} \to \mathsf{DeV^S}$ is a covariant functor, and we have:

\begin{proposition}\label{prop:B in subs5 then NI(B) in devs}
If $\mathbf{B} \in \mathsf{SubS5^S}$, then $\mathcal{NI}(\mathbf{B}) \in \mathsf{DeV^S}$.
\end{proposition}

\begin{remark}\label{rem:prec on NIB}
Since $\prec$ on ${\mathcal{NI}}(\mathbf{B})$ is the restriction of $\prec$ on ${\mathcal{SI}}(\mathbf{B})$, by Lemma~\ref{lem:well-inside} we have that $I \prec J$ iff $U(I) \cap J \neq \varnothing$ for all $I, J \in {\mathcal{NI}}(\mathbf{B})$.
\end{remark}

\begin{definition}\label{def:NI(B)}
Let $\mathbf{B}=(B,S)$ be an $\mathsf{S5}$-subordination algebra. We call $\mathcal{NI}(\mathbf{B})$ the \emph{MacNeille completion} of $\mathbf{B}$. We say that an S-ideal $I$ of $\mathbf{B}$ is \emph{normal} if $I \in {\mathcal{NI}}(\mathbf{B})$.
\end{definition}

\begin{remark}
The terminology of Definition~\ref{def:NI(B)} is an adaptation of the standard terminology for MacNeille completions. Indeed, the construction $\mathcal{NI}(\mathbf{B})$ generalizes  MacNeille completions of boolean algebras to $\mathsf{S5}$-subordination algebras.
\end{remark}

The next theorem provides a characterization of normal S-ideals.

\begin{theorem}\label{thm:NI booleanization of SI}
Let $I \in {\mathcal{SI}}(\mathbf{B})$. We have that $I \in {\mathcal{NI}}(\mathbf{B})$ iff $I=S^{-1}[L(S[U(I)])]$.
\end{theorem}

\begin{proof}
By Lemmas~\ref{lem:operators and negations} and~\ref{lem: pseudocomplement},
\begin{align*}
I^{**} &=\neg S[U(\neg S[U(I)])]=\neg S[\neg L(S[U(I)])]=\neg \neg S^{-1}[L(S[U(I)])]=S^{-1}[L(S[U(I)])]. \qedhere
\end{align*}
\end{proof}

An important feature of the MacNeille completion of an $\mathsf{S5}$-subordination algebra $\mathbf{B}$ is that it is isomorphic to $\mathbf{B}$ in $\mathsf{SubS5^S}$. This happens because morphisms in $\mathsf{SubS5^S}$
are not structure-preserving bijections (see \cite[Rem.~7.1]{ABC22}). Let $Q_{\mathbf{B}} \colon \mathbf{B} \to \mathcal{NI}(\mathbf{B})$ be the relation defined by
\[
a \, Q_{\mathbf{B}} \, I \iff a \in I.
\]

\begin{lemma}
	$Q_{\mathbf{B}}$ is a morphism in $\mathsf{SubS5^S}$.
\end{lemma}

\begin{proof}
	It is easy to see that $Q_{\mathbf{B}}$ is a subordination relation.
	The equality $Q_{\mathbf{B}} = Q_{\mathbf{B}} \circ S$ follows from $I = S^{-1}[I]$. We prove $\prec \circ \, Q_{\mathbf{B}} = Q_{\mathbf{B}}$. For the inclusion $\subseteq$, let $a \in B$ and $I, J \in \mathcal{NI}(\mathbf{B})$ such that $a \mathrel{Q}_{\mathbf{B}} I$ and $I \prec J$. Then $a \in I$ and $I \subseteq J$. Therefore, $a \in J$ which yields $a \mathrel{Q}_{\mathbf{B}} J$.
	For the inclusion $\supseteq$, let $a \in B$ and $I \in \mathcal{NI}(\mathbf{B})$ with $a \mathrel{Q}_{\mathbf{B}} I$.
	Then $a \in I$.
	Since $I$ is an S-ideal, there is $b\in I$ such that $a \mathrel{S} b$.
	We have $a \in S^{-1}[b]$ and $b \in U(S^{-1}[b])$.
Thus, $S^{-1}[b] \prec I$ by Lemma~\ref{lem:well-inside}.
	Consequently, $a \in (S^{-1}[b])^{**} \prec I$ which yields $a \mathrel{(\prec \circ \mathrel{Q}_{\mathbf{B}})} I$ because $(S^{-1}[b])^{**} \in \mathcal{NI}(\mathbf{B})$.
\end{proof}

If $T\colon\mathbf{A} \to \mathbf{B}$ is a morphism in $\mathsf{SubS5^S}$, define $\inv{T}\colon\mathbf{B}\to\mathbf{A}$ by
\begin{equation}\label{eq:T inv}
b\mathrel{\inv{T}}a \mbox{ iff } \neg a \mathrel{T} \neg b.
\end{equation}
Then $\inv{T}$ is a morphism in $\mathsf{SubS5^S}$ by \cite[Rem.~5.11]{ABC22}.

\begin{lemma}\label{thm:iso}
	$Q_{\mathbf{B}} \colon \mathbf{B} \to \mathcal{NI}(\mathbf{B})$ is an isomorphism.
\end{lemma}

\begin{proof}
	Let $T = \inv{Q_{\mathbf{B}}} \colon \mathcal{NI}(\mathbf{B}) \to \mathbf{B}$. By Lemma~\ref{lem: pseudocomplement},
	\begin{equation}\label{QA}
	I \mathrel{T} a \iff \neg a \mathrel{Q_{\mathbf{B}}} I^* \iff \neg a \in \neg S[U(I)] \iff a \in S[U(I)].
	\end{equation}
	We show that $Q_{\mathbf{B}}$ and $T$ are inverses of each other.
	For this we need to prove that $T \circ Q_{\mathbf{B}} = S$ and $Q_{\mathbf{B}} \circ T = \, \prec$.

	We first show that $T \circ Q_{\mathbf{B}} = S$.
	For the inclusion $\subseteq$,
	let $a,b \in B$, $I \in \mathcal{NI}(\mathbf{B})$, and $a \mathrel{Q}_{\mathbf{B}} I \mathrel{T}  b$. Then $a \in I$ and $b \in S[U(I)]$ by \eqref{QA}.
	Thus, $a \mathrel{S} b$.
	For the inclusion $\supseteq$, let $a,b \in B$ with $a \mathrel{S} b$.
	By \eqref{S7}, there is $c \in B$ with $a \mathrel{S} c \mathrel{S} b$.
	Since $c \in U(S^{-1}[c])$, we have $b \in S[U(S^{-1}[c])]$. Let $I=(S^{-1}[c])^{**}$. Then $I \in\mathcal{NI}(\mathbf{B})$ and
	\[
	\neg b \in \neg S[U(S^{-1}[c])]= (S^{-1}[c])^*=(S^{-1}[c])^{***}=I^*= \neg S[U(I)],
	\]
	which implies $I \mathrel{T} b$ by \eqref{QA}. Since $a \in S^{-1}[c] \subseteq I$, we conclude that $a \mathrel{Q}_{\mathbf{B}} I \mathrel{T} b$.

	We next show that $Q_{\mathbf{B}} \circ T = \, \prec$.
	Let $I, J \in \mathcal{NI}(\mathbf{B})$.
	By Lemma~\ref{lem:well-inside} and \eqref{QA},
	\begin{align*}
	I \prec J & \iff U(I) \cap J \neq \varnothing \iff U(I) \cap S^{-1}[J] \neq \varnothing \iff S[U(I)] \cap J \neq \varnothing\ \\
	& \iff \exists a \in S[U(I)] \cap J \iff \exists a \in B : I \mathrel{T} a \mathrel{Q}_{\mathbf{B}} J \iff I \mathrel{(Q_{\mathbf{B}} \circ T)} J.
	\end{align*}
	Thus, $Q_{\mathbf{B}} \colon \mathbf{B} \to \mathcal{NI}(\mathbf{B})$ is an isomorphism.
\end{proof}

\begin{proposition}\label{thm:Q nat iso}
Let $\Delta\colon  \mathsf{DeV^S} \to \mathsf{SubS5^S}$ be the inclusion functor. Then $Q \colon 1_{\mathsf{SubS5^S}} \to \Delta \circ{\mathcal{NI}}$ is a natural isomorphism.
\end{proposition}

\begin{proof}
Let
$T \colon \mathbf{B}_1 \to \mathbf{B}_2$
be a morphism in $\mathsf{SubS5^S}$. By Lemma~\ref{thm:iso}, it is sufficient to show that ${\mathcal{NI}}(T) \circ Q_{\mathbf{B}_1} = Q_{\mathbf{B}_2} \circ T$. (Since $\Delta$ is the inclusion functor, we omit it from the diagram.)
\[
\begin{tikzcd}
\mathbf{B}_1 \arrow[d, "T"'] \arrow[r, "Q_{\mathbf{B}_1}"] &  {\mathcal{NI}}(\mathbf{B}_1) \arrow[d, "{\mathcal{NI}}(T)"] \\
\mathbf{B}_2 \arrow[r, "Q_{\mathbf{B}_2}"] & {\mathcal{NI}}(\mathbf{B}_2)
\end{tikzcd}
\]
Let $a \in B_1$ and $I \in {\mathcal{NI}}(\mathbf{B}_2)$.
We have
\[
a \mathrel{({\mathcal{NI}}(T) \circ Q_{\mathbf{B}_1})} I \mbox{ iff } \exists J \in {\mathcal{NI}}(\mathbf{B}_1) : a \in J \mbox{ and } J \prec T^{-1}[I],
\]
and
\[
a \mathrel{(Q_{\mathbf{B}_2} \circ T)} I \mbox{ iff } \exists b \in B_2 : a \mathrel{T} b \mbox{ and } b \in I  \mbox{ iff } a \in T^{-1}[I].
\]
From this it is clear that if $a \mathrel{({\mathcal{NI}}(T) \circ Q_{\mathbf{B}_1})} I$, then $a \mathrel{(Q_{\mathbf{B}_2} \circ T)} I$. For the converse,
suppose that $a \in T^{-1}[I]$. Since $T^{-1}[I]$ is an S-ideal, there is $b \in T^{-1}[I]$ with $a \mathrel{S}_1 b$. Therefore, $b \in U(S_1^{-1}[b]) \cap T^{-1}[I]$, and so $S_1^{-1}[b] \prec T^{-1}[I]$ by Lemma~\ref{lem:well-inside}. Let $J = (S_1^{-1}[b])^{**}$. Then $J \in {\mathcal{NI}}(\mathbf{B}_1)$, $a \in J$, and $J \prec T^{-1}[I]$.
\end{proof}

\begin{theorem} \label{thm: NI equivalence}
The functors ${\mathcal{NI}} \colon \mathsf{SubS5^S} \to \mathsf{DeV^S}$ and $\Delta \colon \mathsf{DeV^S} \to \mathsf{SubS5^S}$ are quasi-inverses of each other.
Thus, $\mathsf{SubS5^S}$ and $\mathsf{DeV^S}$ are equivalent.
\end{theorem}

\begin{proof}
By Proposition~\ref{thm:Q nat iso}, $Q \colon 1_{\mathsf{SubS5^S}} \to \Delta \circ{\mathcal{NI}}$ is a natural isomorphism.
For the same reason, we have a natural isomorphism $Q' \colon 1_{\mathsf{DeV^S}} \to {\mathcal{NI}} \circ \Delta$ whose component on $\mathbf{B} \in \mathsf{DeV^S}$ is $Q_\mathbf{B}$.
Thus, $\Delta\colon  \mathsf{DeV^S} \to \mathsf{SubS5^S}$ is the quasi-inverse of ${\mathcal{NI}}$.
\end{proof}

\begin{proposition}\label{prop:MacNeille and compingent}
Let $\mathbf{B} = (B,S)$ be an $\mathsf{S5}$-subordination algebra.
\begin{enumerate}[label=\normalfont(\arabic*), ref = \arabic*]
\item\label{prop:MacNeille and compingent:item1} If $\mathbf{B}$ is a compingent algebra, then there is a boolean isomorphism between ${\mathcal{NI}}(\mathbf{B})$ and the usual MacNeille completion $\overline{B}$ of $B$.
\item\label{prop:MacNeille and compingent:item2} If $\mathbf{B}$ is a de Vries algebra, then there is a structure-preserving bijection between $\mathbf{B}$ and ${\mathcal{NI}}(\mathbf{B})$.
\end{enumerate}
\end{proposition}

\begin{proof}
\eqref{prop:MacNeille and compingent:item1}. Since $\mathbf{B}$ is a compingent algebra, it follows from~\cite[Thm.~1.1.4]{deV62} that each $b \in B$ is the supremum of $S^{-1}[b]$. We use this fact to prove that
\begin{equation}\label{eq:US-1I=UI}
U(S^{-1}[I]) = U(I)
\end{equation}
for each ideal $I$ of $B$.
Since $S^{-1}[I] \subseteq I$, we have $U(I) \subseteq U(S^{-1}[I])$. For the reverse inclusion, let $a \in U(S^{-1}[I])$. We show that $a \in U(I)$. Let $b \in I$. Then $S^{-1}[b] \subseteq S^{-1}[I]$. Therefore, $a \in U(S^{-1}[b])$, so $a \ge \bigvee S^{-1}[b]=b$. Thus, $a \in U(I)$. This proves \eqref{eq:US-1I=UI}. A similar argument proves that
\begin{equation}\label{eq:LSF=LF}
L(S[F]) = L(F)
\end{equation}
for each filter $F$ of $B$.
	By \eqref{eq:US-1I=UI} and \eqref{eq:LSF=LF}, for every normal
	ideal $I$ of $B$, we have
	\[
	L(S[U(S^{-1}[I])]) = L(S[U(I)]) = L(U(I)) = I.
	\]
	Thus, applying $S^{-1}$ to both sides yields
	\[
	S^{-1}[L(S[U(S^{-1}[I])])] = S^{-1}[I].
	\]
	This shows, by Theorem~\ref{thm:NI booleanization of SI}, that $S^{-1}[I] \in {\mathcal{NI}}(\mathbf{B})$ for every normal
	ideal $I$ of $B$.
	This defines an order-preserving map $\alpha \colon \overline{B} \to {\mathcal{NI}}(\mathbf{B})$.

	Conversely, for every $I \in {\mathcal{NI}}(\mathbf{B})$, we have that
	$L(U(I))$ is a normal
	ideal of $A$.
	This defines an order-preserving map $\beta \colon {\mathcal{NI}}(\mathbf{B}) \to \overline{B}$.
	By \eqref{eq:US-1I=UI}, for a normal ideal $I$ of $B$, we have
	\[
	L(U(S^{-1}[I])) = L(U(I)) = I.
	\]
	For a normal S-ideal $I$, by \eqref{eq:US-1I=UI} and Theorem~\ref{thm:NI booleanization of SI}, we have
	\[
	S^{-1}[L(U(I))] = S^{-1}[L(S[U(I)]) = I.
	\]
Thus, $\alpha$ and $\beta$ are order-isomorphisms, hence boolean isomorphisms.

\eqref{prop:MacNeille and compingent:item2}.
It is well known~\cite[Thm.~22]{GH09} that sending $b$ to the downset
${\downarrow} b \coloneqq \{ a \in B \mid a \le b \}$
gives a boolean embedding of $B$ into $\overline{B}$, which is an isomorphism iff $B$ is complete. Composing with $\alpha$ yields the boolean embedding $\iota \colon B \to {\mathcal{NI}}(\mathbf{B})$ given by $\iota(b)=S^{-1}[b]$. If $\mathbf{B}$ is a de Vries algebra, then $\iota$ becomes a boolean isomorphism.
It is left to prove that $a \mathrel{S} b$ iff $\iota(a) \prec \iota(b)$. If $a \mathrel{S} b$, then $a \in U(\iota(a)) \cap \iota(b)$, so $\iota(a) \prec \iota(b)$ by Remark~\ref{rem:prec on NIB}. Conversely, if $\iota(a) \prec \iota(b)$, then $U(\iota(a)) \cap \iota(b) \neq \varnothing$, so there exists $c \in U(\iota(a)) \cap \iota(b)$. Since $a$ is the supremum of $\iota(a) = S^{-1}[a]$, we have that $a \le c \mathrel{S} b$, and hence $a \mathrel{S} b$.
Thus, $\iota$ is a structure-preserving bijection between $\mathbf{B}$ and ${\mathcal{NI}}(\mathbf{B})$.
\end{proof}

\begin{remark}
Let $\mathbf{B}$ be a compingent algebra. Then $Q_{\mathbf{B}} \colon \mathbf{B} \to {\mathcal{NI}}(\mathbf{B})$ and $\iota \colon \mathbf{B} \to {\mathcal{NI}}(\mathbf{B})$ are related as follows:
\[
a \mathrel{Q}_{\mathbf{B}} I \iff \iota(a) \prec I
\]
for each $a \in B$ and $I \in {\mathcal{NI}}(\mathbf{B})$. Indeed, since $\mathbf{B}$ is a compingent algebra, $a = \bigvee S^{-1}[a]$, so ${\uparrow} a = U(S^{-1}[a])$, and hence
\[
a \mathrel{Q}_{\mathbf{B}} I \iff a \in I \iff {\uparrow} a \cap I \neq \varnothing \iff U(S^{-1}[a]) \cap I \neq \varnothing \iff \iota(a) \prec I.
\]
\end{remark}

Let $L \in {\mathsf{KRFrm^P}}$. By \cite[Rem.~3.10]{Bez12}, the map $f_L \colon L \to {\mathcal{SI}}({\mathfrak{B}} L)$ given by
\[
f_L(a) = \{ b \in {\mathfrak{B}} L \mid b \prec a \}
\]
is an isomorphism of frames.

\begin{proposition}\label{prop:f nat iso}
$f\colon  1_{{\mathsf{KRFrm^P}}} \to {\mathcal{SI}} \circ \Delta \circ {\mathfrak{B}}$ is a natural isomorphism.
\end{proposition}

\begin{proof}
Let $\Box \colon L \to M$ be a preframe homomorphism and $T={\mathfrak{B}}(\Box)$. Because each $f_L$ is an isomorphism, it is enough to show that ${\mathcal{SI}}(T) \circ f_L = f_M \circ \Box$. (Since $\Delta$ is the inclusion functor, we omit it from the diagram.)
\[
\begin{tikzcd}
L \arrow[d, "\Box"'] \arrow[r, "f_L"] &  {\mathcal{SI}}({\mathfrak{B}} L) \arrow[d, "{\mathcal{SI}}(T)"] \\
M \arrow[r, "f_M"] & {\mathcal{SI}}({\mathfrak{B}} M)
\end{tikzcd}
\]
Let $a \in L$.
We have
\begin{align*}
{\mathcal{SI}}(T)(f_L(a)) = T^{-1}[f_L(a)] & = \{ b \in {\mathfrak{B}} M \mid \exists c \in {\mathfrak{B}} L : b \mathrel{T} c, \ c \prec a \}\\
& = \{ b \in {\mathfrak{B}} M \mid \exists c \in {\mathfrak{B}} L : b \prec \Box c, \ c \prec a  \},
\end{align*}
and $f_M(\Box a) = \{ b \in {\mathfrak{B}} M \mid b \prec \Box a \}$. An argument similar to the proof of Lemma~\ref{lem:boolf compatible} yields
\[
\{ b \in {\mathfrak{B}} M \mid \exists c \in {\mathfrak{B}} L : b \prec \Box c, \ c \prec a \} = \{ b \in {\mathfrak{B}} M \mid b \prec \Box a \},
\]
completing the proof.
\end{proof}

\begin{theorem} \label{thm:dual-equivalence}
\mbox{}\begin{enumerate}[label=\normalfont(\arabic*), ref = \arabic*]
\item\label{thm:dual-equivalence:item1} ${\mathcal{SI}}$ and $\Delta \circ {\mathfrak{B}}$ form a dual equivalence between $\mathsf{SubS5^S}$ and ${\mathsf{KRFrm^P}}$.
\item\label{thm:dual-equivalence:item2}  $\mathcal{SI} \circ \Delta$ and $\mathfrak{B}$ form a dual equivalence between $\mathsf{DeV^S}$ and ${\mathsf{KRFrm^P}}$.
\end{enumerate}
We thus obtain the following diagram of equivalences and dual equivalences that commutes up to natural isomorphism.
\[
\begin{tikzcd}[column sep=6ex, row sep=6ex]
& \mathsf{SubS5^S} \arrow[dl, "{\mathcal{SI}}"'] \arrow[dr, shift left=1ex, "{\mathcal{NI}}"] & \\
{\mathsf{KRFrm^P}} \arrow[rr, "{\mathfrak{B}}"] & & \mathsf{DeV^S} \arrow[ul, hookrightarrow, shift left=0.5ex, "\Delta"]
\end{tikzcd}
\]
\end{theorem}

\begin{proof}
\eqref{thm:dual-equivalence:item1}. By definition of ${\mathcal{NI}}$, we have $\Delta \circ {\mathfrak{B}} \circ {\mathcal{SI}} = \Delta \circ {\mathcal{NI}}$. Therefore, $Q \colon 1_{\mathsf{SubS5^S}} \to \Delta \circ {\mathfrak{B}} \circ {\mathcal{SI}}$ is a natural isomorphism by Proposition~\ref{thm:Q nat iso}. Moreover, $f\colon  1_{{\mathsf{KRFrm^P}}} \to {\mathcal{SI}} \circ \Delta \circ {\mathfrak{B}}$ is a natural isomorphism by Proposition~\ref{prop:f nat iso}. Thus, $\Delta \circ {\mathfrak{B}} \colon {\mathsf{KRFrm^P}} \to \mathsf{SubS5^S}$ is the quasi-inverse of ${\mathcal{SI}}$.

\eqref{thm:dual-equivalence:item2}. By Proposition~\ref{thm:Q nat iso}, $Q \colon 1_{\mathsf{SubS5^S}} \to \Delta \circ {\mathfrak{B}} \circ {\mathcal{SI}}$ is a natural isomorphism.
For the same reason, we have a natural isomorphism $Q' \colon 1_{\mathsf{DeV^S}} \to {\mathfrak{B}} \circ {\mathcal{SI}} \circ \Delta$ whose component on $\mathbf{B} \in \mathsf{DeV^S}$ is $Q_\mathbf{B}$.
Thus, ${\mathfrak{B}} \colon {\mathsf{KRFrm^P}} \to \mathsf{DeV^S}$ is the quasi-inverse of ${\mathcal{SI}} \circ \Delta$.
\end{proof}

By Lemma~\ref{thm:iso}, every $\mathsf{S5}$-subordination algebra is isomorphic to a de Vries algebra. Consequently, Theorem~\ref{thm: NI equivalence}
gives a direct choice-free proof that $\mathsf{SubS5^S}$ is equivalent to $\mathsf{DeV^S}$. Since the category $\mathsf{Comp^S}$ is a full subcategory of $\mathsf{SubS5^S}$ that contains $\mathsf{DeV^S}$, it follows that $\mathsf{Comp^S}$ is equivalent to both $\mathsf{SubS5^S}$ and $\mathsf{DeV^S}$.

\section{Dual descriptions of the completions}\label{sec: dually}

In this section we give dual descriptions of the ideal and MacNeille completions of $\mathsf{S5}$-subordination algebras.

Recall that if $B$ is a boolean algebra and $X={\mathsf{Ult}}(B)$, then the isomorphism $\varphi \colon B \to {\mathsf{Clop}}(X)$ is given by the Stone map $\varphi(a) = \{ x \in X \mid a \in x \}$. This isomorphism induces an
order-isomorphism $\Phi$ between the frame of ideals of $B$ and the frame of open subsets of $X$, as well as an order-isomorphism $\Psi$ between the frame of filters of $B$ and the frame of closed subsets of $X$ ordered by reverse inclusion (see, e.g., \cite[Thm.~33]{GH09}). The isomorphisms are defined as follows:
\begin{equation*}
\Phi(I)=\bigcup\{\varphi(a)\mid a\in I\} \quad \mbox{and} \quad \Psi(F)=\bigcap\{\varphi(a)\mid a\in F\}.
\end{equation*}
It belongs to folklore that for an ideal $I$ and filter $F$ of $B$, we have
\begin{equation}\label{eq:phi psi negation}
\begin{array}{lll}
& \Phi(\neg F)=\Psi(F)^c, \qquad & \Phi(L(F))={\mathsf{int}}\, (\Psi(F)), \\
& \Psi(\neg I)=\Phi(I)^c, \qquad & \Psi(U(I))={\mathsf{cl}}\, (\Phi(I)).
\end{array}
\end{equation}
For the reader's convenience, we give a proof of $\Psi(U(I))={\mathsf{cl}}\, (\Phi(I))$. The other three equalities are proved similarly.
Since $b \in U(I)$ iff $\varphi(a) \subseteq \varphi(b)$ for each $a \in I$, we have
\begin{align*}
	\Psi(U(I)) & = \bigcap \{ \varphi(b) \mid b \in U(I) \} = \bigcap \{ \varphi(b) \mid \Phi(I) \subseteq \varphi(b) \} ={\mathsf{cl}} (\Phi(I)),
\end{align*}
where the last equality follows from the fact that $X$ is a Stone space, hence the closure of a set is the intersection of the clopen subsets containing it.

\begin{definition}
Let $R$ be a binary relation on a set $X$ and $U \subseteq X$. Following the standard notation in modal logic, we set $\Box_R U = X\setminus R^{-1}[X\setminus U]$.
If $R$ is an equivalence relation, we say that $U$ is \emph{$R$-saturated} if $R[U]=U$.
\end{definition}

\begin{remark}\label{rem:box}
\mbox{}\begin{enumerate}
\item\label{rem:box:item1} If $R$ is a closed relation and $U$ is open, then $\Box_R U$ is open.
\item\label{rem:box:item2} If $R$ is an equivalence relation, then $\Box_R U = X\setminus R[X\setminus U]$ and is the largest $R$-saturated subset of $U$. Therefore, $U$ is $R$-saturated iff $\Box_R U=U$.
\end{enumerate}
\end{remark}

Let $(B,S)$ be an $\mathsf{S5}$-subordination algebra. We recall from Remark~\ref{rem:functors equivalences}\eqref{i:functor-Ult} that the $\mathsf{S5}$-subordination space of $(B,S)$ is $(X,R_S)$ where $X$ is the Stone space of $B$ and $R_S$ is given by $x \mathrel{R}_S y$ iff $S[x] \subseteq y$. For simplicity, we write $(X,R)$ instead of $(X,R_S)$.

\begin{lemma}\label{lem:S and * dually}
Let $(B,S)$ be an $\mathsf{S5}$-subordination algebra and $(X,R)$ its $\mathsf{S5}$-subordination space.
\begin{enumerate}[label=\normalfont(\arabic*), ref = \arabic*]
\item \label{i:ideal} If $I$ is an ideal of $B$, then $\Phi(S^{-1}[I])=\Box_{R} \Phi(I)$.
\item \label{i:filter} If $F$ is a filter of $B$, then $\Psi(S[F])=R[\Psi(F)]$.
\end{enumerate}
\end{lemma}

\begin{proof}
\eqref{i:ideal}.
We have
\begin{align*}
\Phi(S^{-1}[I]) &= \bigcup \{ \varphi(a) \mid a \in S^{-1}[I] \} = \bigcup \{ \varphi(a) \mid \exists \, b \in I : a \mathrel{S} b \}\\
&=\bigcup \{ \varphi(a) \mid \exists \, b \in I : R[\varphi(a)] \subseteq \varphi(b) \} = \bigcup \{ \varphi(a) \mid R[\varphi(a)] \subseteq \Phi(I) \}\\
&= \bigcup \{ \varphi(a) \mid \varphi(a) \subseteq\Box_R \Phi(I) \} = \Box_R \Phi(I),
\end{align*}
where the third equality follows from the fact that $a \mathrel{S} b$ iff $R[\varphi(a)] \subseteq \varphi(b)$ (see \cite[Lem.~3.3(2)]{ABC22}); the fourth from the fact that $R[\varphi(a)]$ is closed, hence compact in $X$; and the last equality from the fact that $\Box_R \Phi(I)$ is open and $\{ \varphi(a) \mid a \in B\}$ forms a basis for $X$.

\eqref{i:filter}. It follows from~\eqref{i:ideal}, Lemma~\ref{lem:operators and negations}, Remark~\ref{rem:box}\eqref{rem:box:item2}, and the equations in \eqref{eq:phi psi negation} that
\[
\Psi(S[F])=(\Phi(\neg S[F]))^c=(\Phi(S^{-1}[\neg F]))^c=(\Box_R\Phi(\neg F))^c=(\Box_R(\Psi(F)^c))^c=R[\Psi(F)]. \qedhere
\]
\end{proof}

We recall from the introduction that ${\mathcal{O}}(X)$ denotes the frame of open subsets of a topological space $X$.
Since the set of open $R$-saturated subsets of an $\mathsf{S5}$-subordination space $(X,R)$ forms a subframe of ${\mathcal{O}}(X)$, it is a frame.

\begin{definition}
For an $\mathsf{S5}$-subordination space $\mathbf X=(X,R)$ let ${\mathcal{O}}_R(\mathbf X)$ be the frame of open $R$-saturated subsets of $\mathbf X$.
\end{definition}

\begin{lemma}\label{lem: SI(B) iso to ORS(Ult(B))}
Let $\mathbf B=(B,S)$ be an $\mathsf{S5}$-subordination algebra and $\mathbf X=(X,R)$ its $\mathsf{S5}$-subordination space.
An ideal $I$ of $B$ is an S-ideal iff $\Phi(I)$ is an open $R$-saturated subset of $\mathbf X$.
Therefore, ${\mathcal{SI}}(\mathbf B)$ is isomorphic to ${\mathcal{O}}_R(\mathbf X)$.
\end{lemma}

\begin{proof}
We have that $I$ is an S-ideal iff $I=S^{-1}[I]$. Since $\Phi$ is an isomorphism, Lemma~\ref{lem:S and * dually}\eqref{i:ideal} implies that $I$ is an S-ideal iff $\Phi(I) = \Box_R \Phi(I)$. Therefore, $I$ is an S-ideal iff $\Phi(I)$ is $R$-saturated.
Thus, the restriction of $\Phi$ is an isomorphism from ${\mathcal{SI}}(\mathbf B)$ to ${\mathcal{O}}_R(\mathbf X)$.
\end{proof}

Let $(X,R)$ be an $\mathsf{S5}$-subordination space and $\pi \colon X \to X/R$ the quotient map $\pi(x)=[x]$.

\begin{lemma} \label{lem: OR(X) iso to O(X/R)}
	Let $\mathbf X=(X,R)$ be an $\mathsf{S5}$-subordination space. Then ${\mathcal{O}}_R(\mathbf X)$ is isomorphic to ${\mathcal{O}}(X/R)$.
\end{lemma}

\begin{proof}
Define $f \colon {\mathcal{O}}_R(\mathbf X) \to {\mathcal{O}}(X/R)$ by $f(U)=\pi[U]$ for each $U \in {\mathcal{O}}_R(\mathbf X)$. It follows from the definition of the quotient topology on $X/R$ that $f$ is an isomorphism whose inverse $g \colon {\mathcal{O}}(X/R) \to {\mathcal{O}}_R(\mathbf X)$ is given by $g(V)=\pi^{-1}[V]$.
\end{proof}

Combining Lemmas~\ref{lem: SI(B) iso to ORS(Ult(B))} and~\ref{lem: OR(X) iso to O(X/R)} yields the following result, which by Isbell duality gives an alternative proof of Proposition~\ref{prop:RI compact regular}.

\begin{theorem}
Let $\mathbf{B}=(B,S)$ be an $\mathsf{S5}$-subordination algebra and $\mathbf X=(X,R)$ its subordination space. Then
${\mathcal{SI}}(\mathbf{B})$ is isomorphic to ${\mathcal{O}}(X/R)$.
\end{theorem}

We recall that the MacNeille completion of a boolean algebra $B$ is isomorphic to ${\mathcal{RO}}(X)$ where $X$ is the Stone space of $B$ (see, e.g.,~\cite[Thm.~40]{GH09}).
We will generalize this result to the setting of $\mathsf{S5}$-subordination algebras.
Since regular opens are fixpoints of ${\mathsf{int}}\, {\mathsf{cl}}\colon{\mathcal{O}}(X)\to{\mathcal{O}}(X)$, we introduce the notion of an $R$-regular open subset of an $\mathsf{S5}$-subordination space $(X,R)$ by replacing ${\mathsf{int}}$ with $\Box_R \, {\mathsf{int}}$ and ${\mathsf{cl}}$ with $R \, {\mathsf{cl}}$.

\begin{definition}\label{def: R-regular open}
Let $\mathbf X=(X,R)$ be an $\mathsf{S5}$-subordination space.
We say that an open $R$-saturated subset of $X$ is {\em $R$-regular open} if it is a fixpoint of $ \Box_{R}\,{\mathsf{int}}\, R\,{\mathsf{cl}} \colon {\mathcal{O}}_R(\mathbf X)\to{\mathcal{O}}_R(\mathbf X)$. Let ${\mathcal{RO}}_R(\mathbf X)$ be the poset of $R$-regular open subsets of $\mathbf X$.
\end{definition}

\begin{lemma} \label{lem: R-regular open}
Let $\mathbf X=(X,R)$ be an $\mathsf{S5}$-subordination space and $\prec$ the relation on ${\mathcal{RO}}_R(\mathbf X)$ given by $U \prec V$ iff $R[ {\mathsf{cl}} (U)] \subseteq V$. Then ${\mathcal{RO}}_R(\mathbf X)$ is a de Vries algebra isomorphic to ${\mathcal{RO}}(X/R)$.
\end{lemma}

\begin{proof}
We show that the isomorphism $f \colon {\mathcal{O}}_R(X) \to {\mathcal{O}}(X/R)$ defined in Lemma~\ref{lem: OR(X) iso to O(X/R)}
restricts to an isomorphism between ${\mathcal{RO}}_R(\mathbf X)$ and ${\mathcal{RO}}(X/R)$.
Let $U \in {\mathcal{O}}_R(X)$. Since $\pi \colon X \to X/R$ is the quotient map and $X/R$ is compact Hausdorff, we have
\begin{align}\label{eq:frclA=clfA}
f(R[{\mathsf{cl}}(U)])=\pi[R[{\mathsf{cl}}(U)]]=\pi[{\mathsf{cl}}(U)]={\mathsf{cl}}(\pi[U])={\mathsf{cl}}(f(U)).
\end{align}
By definition of $f$, if $V$ is an $R$-saturated subset of $X$, then $f(V^c)=f(V)^c$ and
\begin{align}\label{eq:fBoxintA=intfA}
\begin{split}
f(\Box_R({\mathsf{int}} (V))) &= f(R[{\mathsf{cl}}(V^c)]^c) = f(R[{\mathsf{cl}}(V^c)])^c = {\mathsf{cl}}(f(V^c))^c\\
&= {\mathsf{int}} (f(V^c)^c) = {\mathsf{int}}(f(V)).
\end{split}
\end{align}
Thus, \eqref{eq:frclA=clfA} and \eqref{eq:fBoxintA=intfA} imply $f(\Box_R({\mathsf{int}} (R[{\mathsf{cl}}(U)])))={\mathsf{int}}(f(R[{\mathsf{cl}}(U)])) = {\mathsf{int}} ({\mathsf{cl}}(f(U)))$. It also follows from \eqref{eq:frclA=clfA} that $f$ preserves and reflects the relation $\prec$. Therefore, $f$ is an isomorphism of de Vries algebras.
\end{proof}

\begin{lemma}\label{lem: SI and NI}
Let $\mathbf B=(B,S)$ be an $\mathsf{S5}$-subordination algebra and $\mathbf X=(X,R)$ its subordination space. For an S-ideal $I$ of $\mathbf{B}$, we have\textup:
\begin{enumerate}[label=\normalfont(\arabic*), ref = \arabic*]
\item \label{i:S-ideal} $\Phi(I^*)=\Box_R {\mathsf{int}} (\Phi(I)^c)$.
\item \label{i:normal S-ideal} $\Phi(I^{**})=\Box_R{\mathsf{int}}(R[{\mathsf{cl}}\, \Phi(I)])$.
\item \label{i:iso normal S-ideals and R-regular} $I$ is a normal S-ideal iff $\Phi(I)$ is an $R$-regular open subset.
\end{enumerate}
Consequently, ${\mathcal{NI}}(\mathbf B)$ is isomorphic to ${\mathcal{RO}}_R(\mathbf X)$.
\end{lemma}

\begin{proof}
\eqref{i:S-ideal}. By the equations in \eqref{eq:phi psi negation} and Lemmas~\ref{lem: pseudocomplement} and~\ref{lem:S and * dually}\eqref{i:filter}, and the fact that ${\mathsf{cl}}\, U = ({\mathsf{int}}(U^c))^c$ for any $U \subseteq X$, we have
\begin{align*}
\Phi(I^*) = \Phi(\neg S[U(I)]) = (\Psi(S[U(I)]))^c = (R[\Psi(U(I))])^c = (R[{\mathsf{cl}}\,\Phi(I)])^c = \Box_R {\mathsf{int}} (\Phi(I)^c).
\end{align*}

\eqref{i:normal S-ideal}. By~\eqref{i:S-ideal}, if $I$ is an S-ideal, then $\Phi(I^*)=(R[{\mathsf{cl}}\,\Phi(I)])^c=\Box_R {\mathsf{int}} (\Phi(I)^c)$. Thus,
\begin{equation*}
\Phi(I^{**}) = \Box_R {\mathsf{int}} (\Phi(I^*)^c) = \Box_R {\mathsf{int}} (((R[{\mathsf{cl}}\,\Phi(I)])^c)^c) = \Box_R{\mathsf{int}}(R[{\mathsf{cl}}\, \Phi(I)]).
\end{equation*}

\eqref{i:iso normal S-ideals and R-regular}. This follows from \eqref{i:normal S-ideal} and Definition~\ref{def: R-regular open}.

Finally, since $\Phi$ is an order-isomorphism, its restriction is an isomorphism of the boolean algebras ${\mathcal{NI}}(\mathbf B)$ and ${\mathcal{RO}}_R(\mathbf X)$. Moreover, if $I,J \in {\mathcal{NI}}(\mathbf B)$, then by \eqref{i:S-ideal} and Remark~\ref{rem:box}\eqref{rem:box:item2},
\begin{align*}
I \prec J & \iff I^* \vee J = A \iff \Phi(I^* \vee J)=X \iff \Phi(I^*) \cup \Phi(J)=X\\
& \iff \Box_R {\mathsf{int}} (\Phi(I)^c) \cup \Phi(J)=X \iff R[ {\mathsf{cl}}\, \Phi(I)]^c \cup \Phi(J)=X\\
& \iff R[ {\mathsf{cl}}\, \Phi(I)] \subseteq \Phi(J) \iff \Phi(I) \prec \Phi(J).
\end{align*}
Therefore, $\Phi$ is an isomorphism of de Vries algebras.
\end{proof}

Combining Lemmas~\ref{lem: R-regular open} and~\ref{lem: SI and NI} yields the following result, which gives an alternative proof of
Proposition~\ref{prop:B in subs5 then NI(B) in devs}.

\begin{theorem}
Let $\mathfrak{A}=(A,S)$ be an $\mathsf{S5}$-subordination algebra and $\mathfrak X=(X,R)$ its subordination space. Then
${\mathcal{NI}}(\mathfrak{A})$ is isomorphic to ${\mathcal{RO}}(X/R)$.
\end{theorem}

\section{Continuous subordinations}\label{sec: cont subs}

In Section~\ref{sec:MacNeille} we gave a direct choice-free proof that $\mathsf{SubS5^S}$ is equivalent to $\mathsf{DeV^S}$ and dually equivalent to ${\mathsf{KRFrm^P}}$. Morphisms of each of these categories encode closed relations between compact Hausdorff spaces. In this section we study the wide subcategories of these categories whose morphisms encode continuous relations between compact Hausdorff spaces.

Since $\mathsf{KHaus}^\mathsf{R}$ is equivalent to $\mathsf{StoneE}^\mathsf{R}$, the next lemma motivates our definition of a continuous compatible subordination. We recall that for a relation $R\colon X_1 \to X_2$ its {\em converse} $\conv{R}\colon X_2\to X_1$ is defined by $y \mathrel{\conv{R}} x$ iff $x \mathrel{R} y$. Also, for a subordination $T\colon B_1\to B_2$, we recall that $\inv{T}\colon B_2\to B_1$ is defined by $b \mathrel{\inv{T}} a$ iff $\lnot a \mathrel{T} \lnot b$ (see \eqref{eq:T inv}).

\begin{lemma} \label{t:correspondence continuous rel and sub}
	Let $R \colon (X_1, E_1) \to (X_2, E_2)$ be a morphism in $\mathsf{StoneE}^\mathsf{R}$.
	The following are equivalent.
	\begin{enumerate}[label=\normalfont(\arabic*), ref = \arabic*]
		\item \label{i:continuous-relation}
		The relation $\mathcal{Q}(R) \colon X_1/E_1 \to X_2/E_2$ is a continuous relation.
		\item \label{i:saturated}
		If $V$ is an $E_2$-saturated open in $X_2$, then $R^{-1}[V]$ is open in $X_1$.
		\item \label{i:clopens}
		If $B_1,B_2\subseteq X_2$ are clopen with $E_2[B_1] \subseteq B_2$, then there is clopen $A\subseteq X_1$ such that $R^{-1}[B_1] \subseteq A \subseteq R^{-1}[B_2]$.
		\item \label{i:continuous-algebraic}
		If $B_1,B_2\subseteq X_2$ are clopen with $E_2[B_1] \subseteq B_2$, then there is clopen $A\subseteq X_1$ such that $A \in \inv{S_R}[B_1]$ and $\inv{S_R}[B_2] \subseteq S_{E_1}[A]$.
	\end{enumerate}
\end{lemma}

\begin{proof}

	\eqref{i:continuous-relation}$\Leftrightarrow$\eqref{i:saturated}. This is immediate.

	\eqref{i:saturated}$\Rightarrow$\eqref{i:clopens}.
	Suppose $B_1,B_2\subseteq X_2$ are clopens with $E_2[B_1] \subseteq B_2$.
	Let $V = \Box_{E_2} B_2$.
	Then $V$ is open.
	Since $E_2[B_1] \subseteq B_2$ and $E_2[B_1]$ is $E_2$-saturated, it follows from the definition of $V$ that $E_2[B_1] \subseteq V$, which implies $B_1 \subseteq V$.
	Therefore, $R^{-1}[B_1] \subseteq R^{-1}[V]$.
	The set $R^{-1}[B_1]$ is closed and $R^{-1}[V]$ is open by \eqref{i:saturated}.
	Thus, there is clopen $A\subseteq X_1$ such that $R^{-1}[B_1] \subseteq A \subseteq R^{-1}[V]$.
	Since $V \subseteq B_2$, we have $R^{-1}[V] \subseteq R^{-1}[B_2]$.
	Hence, $A \subseteq R^{-1}[B_2]$.
	This proves \eqref{i:clopens}.

	\eqref{i:clopens}$\Rightarrow$\eqref{i:saturated}.
	Let $V$ be an $E_2$-saturated open subset of $X_2$.
	Since $V = \bigcup\{ B \in {\mathsf{Clop}}(X_2) \mid B \subseteq V \}$, we have
	$R^{-1}[V] = \bigcup \{R^{-1}[B] \mid B \in {\mathsf{Clop}}(X_2), B \subseteq V\}$.
	Therefore, it is enough to prove that for every clopen subset $B$ of $X_2$ contained in $V$, there is an open subset $U_B$ of $X_1$ such that $R^{-1}[B] \subseteq U_B \subseteq R^{-1}[V]$ (because then $R^{-1}[V] = \bigcup \{U_B \mid B \in {\mathsf{Clop}}(X_2), B \subseteq V\}$).
	Let $B$ be a clopen subset of $X_2$ contained in $V$.
	Since $V$ is saturated, $E_2[B] \subseteq V$.
	Because $E_2[B]$ is closed and $V$ is open, there is a clopen subset $B'$ of $X_2$ such that $E_2[B] \subseteq B' \subseteq V$.
	By \eqref{i:clopens}, there is clopen $A\subseteq X_1$ such that $R^{-1}[B] \subseteq A \subseteq R^{-1}[B']$.
	Since $B' \subseteq V$, we have $R^{-1}[B'] \subseteq R^{-1}[V]$, so
	$A \subseteq R^{-1}[V]$.
	Thus, we have found an open subset $A$ of $X_1$ such that $R^{-1}[B] \subseteq A \subseteq R^{-1}[V]$.
	Hence, \eqref{i:saturated} holds.

	\eqref{i:clopens}$\Leftrightarrow$\eqref{i:continuous-algebraic}. This follows from the following two claims.

	\begin{claim}\label{claim:6.2}
		For clopen $A\subseteq X_1$ and $B\subseteq X_2$, we have $R^{-1}[B] \subseteq A$ iff $A \in \inv{S_R}[B]$.
	\end{claim}

	\begin{proof}[Proof of claim]
		This follows from the equality $\inv{S_R} = S_{\conv{R}}$, shown in \cite[Rem.~3.7]{ABC22}.
	\end{proof}

	\begin{claim}
		For clopen $A\subseteq X_1$ and $B\subseteq X_2$, we have $A \subseteq R^{-1}[B]$ iff $\inv{S_R}[B] \subseteq S_{E_1}[A]$.
	\end{claim}

	\begin{proof}[Proof of claim]
		Let $A\subseteq X_1$ and $B\subseteq X_2$ be clopen. Then
		\begin{align*}
			&\inv{S_R}[B] \subseteq S_{E_1}[A]\\
			& \iff \forall A' \in {\mathsf{Clop}}(X_1) \text{ s.t.\ } B \mathrel{\inv{\mathrel{S}_R}} A' \text{ we have } A' \in S_{E_1}[A]\\
			& \iff \forall A' \in {\mathsf{Clop}}(X_1) \text{ s.t.\ } R^{-1}[B] \subseteq A' \text{ we have } E_1[A] \subseteq A' & \text{(by Claim~\ref{claim:6.2})}\\
			& \iff E_1[A] \subseteq \bigcap \{ A' \in {\mathsf{Clop}}(X_1) \mid R^{-1}[B] \subseteq A' \}\\
			& \iff E_1[A] \subseteq R^{-1}[B] & \text{(since $R^{-1}[B]$ is closed)}\\
			& \iff A \subseteq R^{-1}[B] & \text{(since $R^{-1}[B]$ is saturated).}
		\end{align*}
	\end{proof}
This concludes the proof.
\end{proof}

Lemma~\ref{t:correspondence continuous rel and sub} justifies the following definition.

\begin{definition}
Let $T \colon (B_1, S_1) \to (B_2, S_2)$ be a compatible subordination between $\mathsf{S5}$-subordination algebras.
We say that $T$ is \emph{continuous} if the following holds:
\[
\forall b_1, b_2 \in B_2 \text{ with } b_1 \mathrel{S}_2 b_2 \text{ there is } a \in \inv{T}[b_1] \text{ such that } \inv{T}[b_2] \subseteq S_1[a].
\]
\end{definition}

\begin{remark}\label{rem:cont}
$ $
\begin{enumerate}
\item \label{i:cont1}
The continuity of the compatible subordination relation $T$ is equivalent to the following condition:
\begin{equation}\label{eq:T cont1}
\forall b_1, b_2 \in B_2 \text{ with } b_1 \mathrel{S}_2 b_2 \text{ there is } a \in \inv{T}[b_1] \text{ such that } a \in L(\inv{T}[b_2]).
\end{equation}
To see this, it is enough to prove that $\inv{T}[b_2] \subseteq S_1[a]$ is equivalent to $a \in L(\inv{T}[b_2])$. For the left-to-right implication,
by \eqref{S5} we have that $S_1[a] \subseteq U(a)$, and so $\inv{T}[b_2] \subseteq S_1[a]$ implies $\inv{T}[b_2] \subseteq U(a)$, which is equivalent to $a \in L(\inv{T}[b_2])$.
For the right-to-left implication, suppose $a \in L(\inv{T}[b_2])$ and let $a' \in \inv{T}[b_2]$.
Since $\inv{T}$ is a compatible subordination, there is $a'' \in \inv{T}[b_2]$ such that $a'' \mathrel{S}_1 a'$.
Therefore, $a \leq a'' \mathrel{S}_1 a'$, which implies $a \mathrel{S}_1 a'$, and hence $a' \in S_1[a]$.

\item \label{i:cont2}
The continuity of
$T$ is also equivalent to the following condition:
\begin{equation}\label{eq:T cont2}
\forall b_1, b_2 \in B_2 \text{ with } b_1 \mathrel{S}_2 b_2 \text{ there is } a \in T^{-1}[b_2] \text{ such that } a \in U(T^{-1}[b_1]).
\end{equation}
Indeed, suppose that \eqref{eq:T cont1} holds, and let $b_1, b_2 \in B_2$ be such that $b_1 \mathrel{S}_2 b_2$.
Then, by \eqref{S6}, $\lnot b_2 \mathrel{S}_2 \lnot b_1$.
Therefore, there is $a \in \inv{T}[\lnot b_2]$ such that $a \in L(\inv{T}[\lnot b_1])$.
The condition $a \in \inv{T}[\lnot b_2]$ is equivalent to $\lnot a \in T^{-1}[b_2]$.
Similarly,
the condition $a \in L(\inv{T}[\lnot b_1])$ is equivalent to $\lnot a \in U(T^{-1}[b_1])$.
Thus, \eqref{eq:T cont1} implies \eqref{eq:T cont2}, and the converse is proved similarly. Consequently, both conditions are equivalent to $T$ being continuous.

\item\label{i:cont3} If $B_1$ is complete, then $T$ is continuous iff
\[
\forall b_1, b_2 \in B_2 \ \left(b_1 \mathrel{S}_2 b_2 \Rightarrow b_1 \mathrel{\inv{T}} \left(\bigwedge \inv{T}[b_2]\right)\right)
\]
iff
\[
\forall b_1, b_2 \in B_2 \ \left(b_1 \mathrel{S}_2 b_2 \Rightarrow \left(\bigvee\mathrel{T}^{-1}[b_1]\right) \mathrel{T} b_2\right).
\]
\end{enumerate}
\end{remark}

\begin{definition}
Let $\mathsf{SubS5^{CS}}$ be the wide subcategory of $\mathsf{SubS5^S}$ whose morphisms are continuous compatible subordinations, and define $\mathsf{Comp^{CS}}$ and $\mathsf{DeV^{CS}}$ similarly.
\end{definition}

\begin{lemma}\label{lem:continuity SI(T) and B(box)}
Let $(B_1,S_1),(B_2,S_2)$ be $\mathsf{S5}$-subordination algebras and $T \colon B_1 \to B_2$ a morphism in $\mathsf{SubS5^S}$. Let also $L_1,L_2$ be compact regular frames and $\Box \colon L_1 \to L_2$ a preframe homomorphism.
\begin{enumerate}[label=\normalfont(\arabic*), ref = \arabic*]
\item\label{lem:continuity SI(T) and B(box):item1} If $T \colon B_1 \to B_2$ is continuous, then ${\mathcal{SI}}(T) \colon {\mathcal{SI}}(B_2,S_2) \to {\mathcal{SI}}(B_1,S_1)$ is a $\mathsf{c}$-morphism.
\item\label{lem:continuity SI(T) and B(box):item2} If $\Box \colon L_1 \to L_2$ is a $\mathsf{c}$-morphism, then ${\mathfrak{B}}(\Box) \colon {\mathfrak{B}}(L_2) \to {\mathfrak{B}}(L_1)$ is  continuous.
\item\label{lem:continuity SI(T) and B(box):item3} If $T \colon B_1\to B_2$ is an isomorphism in $\mathsf{SubS5^S}$, then $T$ is an isomorphism in $\mathsf{SubS5^{CS}}$.
\item\label{lem:continuity SI(T) and B(box):item4} If $\Box \colon L_1\to L_2$ is an isomorphism in ${\mathsf{KRFrm^P}}$, then $\Box$ is an isomorphism in ${\mathsf{KRFrm^C}}$.
\end{enumerate}
\end{lemma}

\begin{proof}
\eqref{lem:continuity SI(T) and B(box):item1}. Let $\Box={\mathcal{SI}}(T)$. Then $\Box$ is a preframe homomorphism by Proposition~\ref{prop:SI(T) preframe hom}. We define $\Diamond \colon {\mathcal{SI}}(B_2,S_2) \to {\mathcal{SI}}(B_1,S_1)$ by
\[
\Diamond I = \{a \in B_1 \mid \exists b \in I : a \in L(\inv{T}[b]) \}.
\]
We first show that $\Diamond$ is well defined. It is straightforward to see that $\Diamond I$ is an ideal of $B_1$. To see that $\Diamond I$ is an S-ideal, let $a\in\Diamond I$. Then there is $b\in I$ with $a\in L(\inv{T}[b])$. Since $I$ is an S-ideal, there is $d\in I$ with $b \mathrel{S}_2 d$. Because $T$ is continuous, there is $c\in \inv{T}[b]$ such that $c \in L(\inv{T}[d])$ (see Remark~\ref{rem:cont}\eqref{i:cont1}). Therefore, $c \in \Diamond I$ since $d \in I$. Because $\inv{T}$ is compatible, from $b \mathrel{\inv{T}} c$ it follows that there is $c' \in \inv{T}[b]$ with $c' \mathrel{S}_1 c$. But then $a \le c'$ since $a \in L(\inv{T}[b])$. Thus, $a \le c' \mathrel{S}_1 c$, so $a \mathrel{S}_1 c$, and hence $\Diamond I$ is an S-ideal.

We next show that $\Diamond$ preserves arbitrary joins. It is straightforward to see that $I \subseteq J$ implies $\Diamond I \subseteq \Diamond J$. Therefore, if $\{ I_\alpha \} \subseteq {\mathcal{SI}}(B_2,S_2)$, then $\bigvee \Diamond I_\alpha \subseteq \Diamond \left( \bigvee I_\alpha \right)$. For the reverse inclusion, let $x \in \Diamond \left( \bigvee I_\alpha \right)$. Then there is $b \in \bigvee I_\alpha$ with $x \in L(\inv{T}[b])$. Since $b \in \bigvee I_\alpha$, there exist $\alpha_1, \ldots, \alpha_n$ and $d_i \in I_{\alpha_i}$ for $i=1, \ldots, n$ such that $b \le d_1 \vee \ldots \vee d_n$. Thus, $x \in L(\inv{T}[d_1 \vee \cdots \vee d_n])$. Since $I_{\alpha_i}$ is an S-ideal for each $i$, it follows that there exist $e_i \in I_{\alpha_i}$ with $d_i \mathrel{S}_2 e_i$ for each $i$. By continuity of $T$, there exist $a_i \in \inv{T}[d_i]$ with $a_i \in L(\inv{T}[e_i])$ for each $i$. So $a_i \in \Diamond I_{\alpha_i}$ for each $i$ and $a_1 \vee \cdots \vee a_n \in \inv{T}[d_1 \vee \cdots \vee d_n]$. Since $x \in L(\inv{T}[d_1 \vee \cdots \vee d_n])$, it follows that $x \le a_1 \vee \cdots \vee a_n$. Consequently, $x \in \bigvee \Diamond I_\alpha$.

It is left to prove that $\Box I \cap \Diamond J \subseteq \Diamond(I \cap J)$ and $\Box(I \vee J) \subseteq \Box I \vee \Diamond J$ for all $I,J \in {\mathcal{SI}}(B_2,S_2)$. Let $x \in \Box I \cap \Diamond J$. Since $x \in \Box I = T^{-1}[I]$, there is $a \in I$ with $x \mathrel{T} a$. Because $x \in \Diamond J$, there is $b \in J$ with $x \in L(\inv{T}[b])$. We first show that $x \in L(\inv{T}[a \wedge b])$. If $e \in \inv{T}[a \wedge b]$, then $\neg e \mathrel{T} (\neg a \vee \neg b)$. Since $x \mathrel{T} a$, it follows that $(x \wedge \neg e) \mathrel{T} (a \wedge (\neg a \vee \neg b))$. So $(x \wedge \neg e) \mathrel{T} (a \wedge \neg b)$, and hence $(x \wedge \neg e) \mathrel{T} \neg b$. Therefore, $\neg x \vee e \in \inv{T}[b]$. Because $x \in L(\inv{T}[b])$, we have $x \le \neg x \vee e$, and so $x \le e$. Thus, $x \in L(\inv{T}[a \wedge b])$. Since $a \wedge b \in I \cap J$, we conclude that $x \in \Diamond(I \cap J)$.

Finally,
let $x \in \Box(I \vee J)=T^{-1}[I \vee J]$. Then there is $y \in I \vee J$ with $x \mathrel{T} y$. Thus, there exist $a \in I$, $b \in J$ with $y \le a \vee b$. Since $I$ and $J$ are S-ideals, there exist $a' \in I$, $b' \in J$ with $a \mathrel{S}_2 a'$ and $b \mathrel{S}_2 b'$. Because $\neg a' \mathrel{S}_2 \neg a$ and $b \mathrel{S}_2 b'$, the continuity of $T$ yields that there exist $c \in \inv{T}[\neg a']$ and $d \in \inv{T}[b]$ with $c \in L(\inv{T}[\neg a])$ and $d \in L(\inv{T}[b'])$. From $c \in \inv{T}[\neg a']$
it follows that $\neg c \mathrel{T} a'$, so $\neg c \in T^{-1}[I] = \Box I$. Since $d \in L(\inv{T}[b'])$ and $b' \in J$, we have $d \in \Diamond J$. Therefore, $\neg c \vee d \in \Box I \vee \Diamond J$. We prove that $x \le \neg c \vee d$, which is equivalent to $c \le \neg x \vee d$. We have $x \mathrel{T} (a \vee b)$ and $\neg d \mathrel{T} \neg b$ because $d \in \inv{T}[b]$. Therefore, $(x \wedge \neg d) \mathrel{T} ((a \vee b) \wedge \neg b)$, and so $(x \wedge \neg d) \mathrel{T} (a \wedge \neg b) \le a$. Thus,
$\neg x \vee d \in \inv{T}[\neg a]$. Since $c \in L(\inv{T}[\neg a])$, we obtain $c \le \neg x \vee d$. Consequently, $x \in \Box I \vee \Diamond J$ because $x \le \neg c \vee d \in \Box I \vee \Diamond J$.

\eqref{lem:continuity SI(T) and B(box):item2}. Let $T = {\mathfrak{B}}(\Box)$. By Lemma~\ref{lem:boolf compatible}, $T \colon {\mathfrak{B}}({L_2})\to{\mathfrak{B}}({L_1})$ is a morphism in $\mathsf{SubS5^S}$. To see that it is continuous, let $b_1,b_2 \in L_1$ with $b_1 \prec b_2$. Set $a = \neg \Box \neg b_2$. Then $a\in{\mathfrak{B}}(L_2)$. We show that $b_1 \mathrel{\inv{T}} a$ and $a \in L(\inv{T}[b_2])$. We have $\neg b_2 \prec \neg b_1$, so
$\Box \neg b_2 \prec \Box \neg b_1$ since $\Box$ preserves $\prec$ (see \cite[Lem.~3.6]{BBH15}). The definition of $\prec$ implies $\neg \neg \Box \neg b_2 \prec \Box \neg b_1$. Therefore, $\neg a \prec \Box \neg b_1$, which gives $\neg a \mathrel{T}  \neg b_1$. Thus, $b_1 \mathrel{\inv{T}} a$. If $x \in \inv{T}[b_2]$, then $\neg x \mathrel{T} \neg b_2$, so $\neg x \prec \Box \neg b_2$. Therefore, $a=\neg \Box \neg b_2 \prec x$, and hence $a \le x$. Thus, $a \in L(\inv{T}[b_2])$, and so $T$ is continuous.

\eqref{lem:continuity SI(T) and B(box):item3}.
This is a consequence of a stronger result proved in Lemma~\ref{lem:functionality SI(T) and B(box)}(\ref{lem:functionality SI(T) and B(box):item3}) below.

\eqref{lem:continuity SI(T) and B(box):item4}. Since $\Box$ is an isomorphism in ${\mathsf{KRFrm^P}}$, it is a poset isomorphism. Defining $\Diamond \coloneqq \Box$ then yields that $\Box$ is an isomorphism in ${\mathsf{KRFrm^C}}$.
\end{proof}

As an immediate consequence of Lemma~\ref{lem:continuity SI(T) and B(box)} we obtain:

\begin{theorem} \label{thm: continuous case}
\mbox{}\begin{enumerate}[label=\normalfont(\arabic*), ref = \arabic*]
\item The dual equivalence between $\mathsf{SubS5^S}$ and ${\mathsf{KRFrm^P}}$ restricts to a dual equivalence between $\mathsf{SubS5^{CS}}$ and ${\mathsf{KRFrm^C}}$.
\item The dual equivalence between $\mathsf{SubS5^S}$ and $\mathsf{DeV^S}$ restricts to a dual equivalence between $\mathsf{SubS5^{CS}}$ and $\mathsf{DeV^{CS}}$.
\end{enumerate}
\end{theorem}

Let $(B_1,S_1)$ and $(B_2,S_2)$ be de Vries algebras. If $T \colon B_1 \to B_2$ is a morphism in $\mathsf{DeV^{CS}}$, we define $\Box_T \colon B_2 \to B_1$ by $\Box_T b = \bigvee T^{-1}[b]$. Also, if $\Box \colon B_2 \to B_1$ is a lower continuous
de Vries multiplicative map, we define $T_\Box \colon B_1 \to B_2$ by
\[
a \mathrel{T}_\Box b \iff \exists b' \ (a \mathrel{S}_1 \Box b'\mbox{ and }b' \mathrel{S}_2 b).
\]

\begin{lemma}\label{lem:continuity BoxT and TBox}
Let $(B_1,S_1)$ and $(B_2,S_2)$ be de Vries algebras.
\begin{enumerate}[label=\normalfont(\arabic*), ref = \arabic*]
\item\label{lem:continuity BoxT and TBox:item1} If $T \colon B_1 \to B_2$ is a morphism in $\mathsf{DeV^{CS}}$, then $\Box_T \colon B_2 \to B_1$ is a lower continuous de Vries multiplicative map.
\item\label{lem:continuity BoxT and TBox:item2} If $\Box \colon B_2 \to B_1$ is a lower continuous de Vries multiplicative map, then $T_\Box \colon B_1 \to B_2$ is a morphism in $\mathsf{DeV^{CS}}$.
\item\label{lem:continuity BoxT and TBox:item3} $\Box_{T_\Box}=\Box$.
\item\label{lem:continuity BoxT and TBox:item4} $T_{\Box_T}=T$.
\end{enumerate}
\end{lemma}

\begin{proof}
\eqref{lem:continuity BoxT and TBox:item1}. We first show that $\Box_T$ is de Vries multiplicative. It is obvious that $\Box_T(1)=1$. Let $b_1 \mathrel{S}_2 b_2$ and $d_1 \mathrel{S}_2 d_2$. Since $T$ is continuous and $B_1$ is complete, by Remark~\ref{rem:cont}\eqref{i:cont3}
\[
\left(\bigvee\mathrel{T}^{-1}[b_1]\right) \mathrel{T} b_2 \quad \mbox{and} \quad \left(\bigvee\mathrel{T}^{-1}[d_1]\right) \mathrel{T} d_2.
\]
Therefore, $(\Box_T b_1 \wedge \Box_T d_1) \mathrel{T} (b_2 \wedge d_2)$. Since $T$ is compatible, there is $x \in B_1$ such that
\[
(\Box_T b_1 \wedge \Box_T d_1) \mathrel{S}_1 x \mathrel{T} (b_2 \wedge d_2).
\]
Thus, $(\Box_T b_1 \wedge \Box_T d_1) \mathrel{S}_1 x \le \Box_T (b_2 \wedge d_2)$, and hence $(\Box_T b_1 \wedge \Box_T d_1) \mathrel{S}_1 \Box_T (b_2 \wedge d_2)$. Consequently, $\Box_T$ is de Vries multiplicative. To see that $\Box_T$ is lower continuous, let $x \in T^{-1}[b]$. Since $T$ is compatible, $x \mathrel{T} y \mathrel{S}_2 b$ for some $y \in B_2$. Therefore, $x \le \Box_T y$, and hence $\Box_T b = \bigvee \{ \Box_T y \mid y \mathrel{S}_2 b \}$.

\eqref{lem:continuity BoxT and TBox:item2}. That $0 \mathrel{T}_\Box 0$ is straightforward and that $1 \mathrel{T}_\Box 1$ follows from $\Box 1 = 1$. Since $\Box$ is lower continuous, it is order preserving (see \cite[Prop.~4.15]{BBH15} and Remark~\ref{rem:box diamond upper lower}).
Suppose $a,a' \mathrel{T}_\Box b$. Then there exist $b_1$ and $b_2$ such that $a \mathrel{S}_1 \Box b_1$, $b_1 \mathrel{S}_2 b$, $a' \mathrel{S}_1 \Box b_2$, and $b_2 \mathrel{S}_2 b$. From $a \mathrel{S}_1 \Box b_1$ and $a' \mathrel{S}_1 \Box b_2$ it follows that $(a \lor a') \mathrel{S}_1 (\Box b_1 \lor \Box b_2) \leq \Box(b_1 \lor b_2)$, and so $(a \lor a') \mathrel{S}_1 \Box(b_1 \lor b_2)$. Also, from $b_1 \mathrel{S}_2 b$ and $b_2 \mathrel{S}_2 b$ it follows that $(b_1 \lor b_2) \mathrel{S}_2 b$. Thus, $(a\vee a') \mathrel{T}_\Box b$.
Next suppose $a \mathrel{T}_\Box b,b'$. Then there exist $b_1$ and $b_2$ such that $a \mathrel{S}_1 \Box b_1$, $b_1 \mathrel{S}_2 b$, $a \mathrel{S}_1 \Box b_2$, and $b_2 \mathrel{S}_2 b'$. From $a \mathrel{S}_1 \Box b_1$ and $a \mathrel{S}_1 \Box b_2$ it follows that $a \mathrel{S}_1 (\Box b_1 \land \Box b_2) = \Box (b_1 \land b_2)$ (see \cite[Prop.~4.15]{BBH15} and Remark~\ref{rem:box diamond upper lower}). Also, from $b_1 \mathrel{S}_2 b$ and $b_2 \mathrel{S}_2 b'$ it follows that $(b_1 \land b_2) \mathrel{S}_2 (b \land b')$. Thus, $a \mathrel{T}_\Box (b \wedge b')$.
Finally, that $a \le a' \mathrel{T}_\Box b' \le b$ implies $a \mathrel{T}_\Box b$ is straightforward. This gives that $T_\Box$ is a subordination.

That $T_\Box \subseteq S_2 \circ T_\Box$ and $T_\Box \subseteq T_\Box \circ S_1$ follow from the fact that $S_2$ and $S_1$ satisfy (\ref{S7}).
The reverse inclusions are obvious, thus $S_2 \circ T_\Box = T_\Box = T_\Box \circ S_1$. This yields that $T_\Box$ is a compatible subordination.

It is left to prove that $T_\Box$ is continuous. Let $b_1 \mathrel{S}_2 b_2$. Then there is $y \in B_2$ with $b_1 \mathrel{S}_2 y \mathrel{S}_2 b_2$. Set $a=\Box b_1$. Since $a \mathrel{S}_1 \Box y$ and $y \mathrel{S}_2 b_2$, we have $a \mathrel{T}_\Box b_2$, so $a \in T_\Box^{-1}[b_2]$. Moreover, if $x \mathrel{T}_\Box b_1$, then there is $z \in B_2$ such that $x \mathrel{S}_1 \Box z$ and $z \mathrel{S}_2 b_1$. Therefore, $x \mathrel{S}_1 \Box b_1$, and so $x \mathrel{S}_1 a$. Thus, $a \in U(T_\Box^{-1}[b_1])$ by \eqref{S5}, and hence $T_\Box$ is continuous by Remark~\ref{rem:cont}\eqref{i:cont2}.

\eqref{lem:continuity BoxT and TBox:item3}. We have
\[
\Box_{T_\Box} b = \bigvee T_\Box^{-1}[b] = \bigvee \{ a \mid \exists b' \ (a \mathrel{S}_1 \Box b' \mbox{ and } b' \mathrel{S}_2 b)\} = \bigvee \{ \Box b' \mid b' \mathrel{S}_2 b \} = \Box b,
\]
where the second to last equality follows from the facts that $S_2$ satisfies (\ref{S7})
and $b' \mathrel{S}_2 b$ implies $\Box b' \mathrel{S}_1 \Box b$, and the last equality from the lower continuity of $\Box$.

\eqref{lem:continuity BoxT and TBox:item4}. We have
\[
a T_{\Box_T} b \iff \exists b' \ (a \mathrel{S}_1 \Box_T b' \mbox{ and } b' \mathrel{S}_2 b) \iff \exists b' \ (a \mathrel{S}_1 \bigvee T^{-1}[b'] \mbox{ and } b' \mathrel{S}_2 b) \iff a \mathrel{T} b,
\]
where the last equivalence follows from Remark~\ref{rem:cont}\eqref{i:cont3} and the fact that $T$ is a morphism in $\mathsf{DeV^{CS}}$.
\end{proof}

As an immediate consequence of Lemma~\ref{lem:continuity BoxT and TBox} we obtain:

\begin{theorem} \label{thm: continuous DeV}
$\mathsf{DeV^{CS}}$ is dually isomorphic to $\mathsf{DeV^C}$.
\end{theorem}

Putting Theorems~\ref{thm: continuous case} and~\ref{thm: continuous DeV} together yields the following version of the commutative diagram of equivalences and dual equivalences given at the end of Section~\ref{sec:MacNeille}.
\[
\begin{tikzcd}[column sep=6ex, row sep=6ex]
& \mathsf{SubS5^{CS}} \arrow[dl, "{\mathcal{SI}}"'] \arrow[dr, shift left=1ex, "{\mathcal{NI}}"] &  &\\
{\mathsf{KRFrm^C}} \arrow[rr, "{\mathfrak{B}}"] & & \mathsf{DeV^{CS}} \arrow[ul, hookrightarrow, shift left=0.5ex, "\Delta"] \arrow[r, leftrightarrow, "d"] & \mathsf{DeV^C}
\end{tikzcd}
\]

Since $\mathsf{Comp^{CS}}$ is a full subcategory of $\mathsf{SubS5^{CS}}$ that contains $\mathsf{DeV^{CS}}$, it follows that $\mathsf{Comp^{CS}}$ is equivalent to both $\mathsf{SubS5^{CS}}$ and $\mathsf{DeV^{CS}}$, and hence dually equivalent to ${\mathsf{KRFrm^C}}$ and $\mathsf{DeV^C}$.

\begin{remark}
As we pointed out in Section~\ref{sec: prelims}, ${\mathsf{KRFrm^C}}$ and $\mathsf{DeV^C}$ are dually equivalent to $\mathsf{KHaus}^\mathsf{C}$. Hence, $\mathsf{SubS5^{CS}}$ and $\mathsf{DeV^{CS}}$ are equivalent to $\mathsf{KHaus}^\mathsf{C}$. We next describe the wide subcategories of $\mathsf{StoneE}^\mathsf{R}$ and $\mathsf{Gle}^\mathsf{R}$ that are equivalent to $\mathsf{KHaus}^\mathsf{C}$.

Let $(X,E)$ be an $\mathsf{S5}$-subordination space. A morphism $R\colon X_1\to X_2$ in $\mathsf{StoneE}^\mathsf{R}$ is {\em continuous} if $R^{-1}[U]$ is open for each $E_2$-saturated open $U \subseteq X_2$. Let $\mathsf{StoneE}^\mathsf{C}$ be the wide subcategory of $\mathsf{StoneE}^\mathsf{R}$ whose morphisms are continuous morphisms in $\mathsf{StoneE}^\mathsf{R}$ and define $\mathsf{Gle}^\mathsf{C}$ similarly. Using Lemma~\ref{t:correspondence continuous rel and sub} it is straightforward to see that the equivalence between $\mathsf{StoneE}^\mathsf{R}$ and $\mathsf{Gle}^\mathsf{R}$ described in
Remark~\ref{rem:functors equivalences}(\ref{i:GleR StoneER equivalence})
restricts to an equivalence between $\mathsf{StoneE}^\mathsf{C}$ and $\mathsf{Gle}^\mathsf{C}$. By \cite[Thm.~4.16]{BezhanishviliGabelaiaEtAl2019}, $\mathsf{Gle}^\mathsf{C}$ is equivalent to $\mathsf{KHaus}^\mathsf{C}$. Thus, each of $\mathsf{KHaus}^\mathsf{C}$, $\mathsf{StoneE}^\mathsf{C}$, and $\mathsf{Gle}^\mathsf{C}$ is equivalent or dually equivalent to each of the categories in the diagram above.
\end{remark}

\section{Functional subordinations}\label{sec:functional}

In this final section we further restrict our attention to continuous functions between compact Hausdorff spaces and their corresponding compatible subordinations.

\begin{definition} \cite[Sec.~8]{ABC22}
\begin{enumerate}
\item Call a morphism $T \colon (B_1,S_1) \to (B_2,S_2)$ in $\mathsf{SubS5^S}$ \emph{functional} if
\[
\inv{T} \circ T \subseteq S_1 \quad \mbox{and} \quad S_2 \subseteq T \circ \inv{T}.
\]
\item Let $\mathsf{SubS5^F}$ be
the wide subcategory of $\mathsf{SubS5^S}$ consisting of functional morphisms, and define $\mathsf{DeV^F}$ and $\mathsf{Comp^F}$ similarly.
\end{enumerate}
\end{definition}

\begin{remark}
If $T$ is functional, then $T$ is continuous. Indeed, let $b_1 \mathrel{S}_2 b_2$. Since $T$ is functional, $S_2 \subseteq T \circ \inv{T}$, so there exists $a \in B_1$ such that $b_1 \mathrel{\inv{T}} a$ and $a \mathrel{T} b_2$. Thus, $a \in \inv{T}[b_1]$. Moreover, if $a' \in \inv{T}[b_2]$, then $b_2 \mathrel{\inv{T}} a'$. Therefore, $a \mathrel{T} b_2 \mathrel{\inv{T}} a'$, so $a \mathrel{S}_1 a'$ because $\inv{T} \circ T \subseteq S_1$ by the functionality of $T$. Consequently, $T$ is continuous. Thus, $\mathsf{SubS5^F}$ is a wide subcategory of $\mathsf{SubS5^{CS}}$. Similarly, $\mathsf{DeV^F}$ and $\mathsf{Comp^F}$ are wide subcategories of $\mathsf{DeV^{CS}}$ and $\mathsf{Comp^{CS}}$, respectively.
\end{remark}

\begin{lemma} \label{l:functional-alternative-def}
	Let $T \colon (B_1, S_1) \to (B_2, S_2)$ be a morphism in $\mathsf{SubS5^S}$.
	The following conditions are equivalent.
	\begin{enumerate}[label=\normalfont(\arabic*), ref = \arabic*]
		\item \label{i:functional} $T$ is functional.
		\item \label{i:new-functional}
		The following hold for all $a \in B_1$ and $b_1, b_2, b_1', b_2' \in B_2$\textup:
		\begin{enumerate}[label=\normalfont(\alph*), ref = 2\alph*]
			\item \label{i:fun-0-ary}
			If $a \mathrel{T} 0$, then $a = 0$.
			\item \label{i:fun-2-ary}
			If $a \mathrel{T} (b_1 \lor b_2)$, $b_1 \mathrel{S}_2 b_1'$, and $b_2 \mathrel{S}_2 b_2'$, then there are $a_1, a_2 \in B_1$ such that $a \mathrel{S}_1 (a_1 \lor a_2)$, $a_1 \mathrel{T} b_1'$, and $a_2 \mathrel{T} b_2'$.
		\end{enumerate}
	\end{enumerate}
\end{lemma}

\begin{proof}
By \cite[Lem.~8.6(1)]{ABC22}, $\inv{T} \circ T \subseteq S_1$ is equivalent to \eqref{i:fun-0-ary}. Therefore, it is sufficient to prove that, under these equivalent conditions, $S_2 \subseteq T \circ \inv{T}$ is equivalent to \eqref{i:fun-2-ary}.

	To prove that $S_2 \subseteq T \circ \inv{T}$ implies \eqref{i:fun-2-ary}, let $a \mathrel{T} (b_1 \lor b_2)$, $b_1 \mathrel{S}_2 b_1'$, and $b_2 \mathrel{S}_2 b_2'$.
	Since $S_2 \subseteq T \circ \inv{T}$, from $b_1 \mathrel{S}_2 b_1'$ and $b_2 \mathrel{S}_2 b_2'$ it follows that there are $a_1, a_2 \in B_1$ such that $b_1 \mathrel{\inv{T}} a_1 \mathrel{T} b_1'$ and $b_2 \mathrel{\inv{T}} a_2 \mathrel{T} b_2'$.
	Therefore, $a \mathrel{T} (b_1 \lor b_2) \mathrel{\inv{\mathrel{T}}} (a_1 \lor a_2)$.
	Since $\inv{T} \circ T \subseteq S_1$,
	it follows that $a \mathrel{S}_1 (a_1 \lor a_2)$.

	To prove that \eqref{i:fun-2-ary} implies $S_2 \subseteq T \circ \inv{T}$,
	let $b_1,b_2 \in B_2$ be such that $b_1 \mathrel{S}_2 b_2$.
By \eqref{S7}, there is $b \in B_2$ such that $b_1 \mathrel{S}_2 b \mathrel{S}_2 b_2$.
	Therefore, $1 \mathrel{T} (\lnot b \lor b)$.
	By \eqref{S6}, $b_1 \mathrel{S}_2 b$ implies $\lnot b \mathrel{S}_2 \lnot b_1$.
	Thus, by \eqref{i:fun-2-ary}, there are $a_1, a_2 \in B_1$ such that $1 \mathrel{S}_1 (a_1 \lor a_2)$, $a_1 \mathrel{T} \lnot b_1$, and $a_2 \mathrel{T} b_2$.
	By \eqref{S5}, from $1 \mathrel{S}_1 (a_1 \lor a_2)$ it follows that $1 = a_1 \lor a_2$, so $\lnot a_1 \leq a_2$.
Since $a_1 \mathrel{T} \lnot b_1$, we have $b_1 \mathrel{\inv{T}} \neg a_1 \le a_2$, and hence $b_1 \mathrel{\inv{T}} a_2$. Because $b_1 \mathrel{\inv{T}} a_2 \mathrel{T} b_2$, it follows that $b_1 \mathrel{(T \circ \inv{T})} b_2$.
	Thus, $S_2 \subseteq T \circ \inv{T}$, completing the proof.
\end{proof}

In order to establish equivalences between various categories of $\mathsf{S5}$-subordination algebras with functional morphisms, we require the following lemma.

\begin{lemma} \label{lem: inv of T}
	Let $(B_1,S_1),(B_2,S_2)$ be $\mathsf{S5}$-subordination algebras. If $T \colon B_1 \to B_2$ is an isomorphism in $\mathsf{SubS5^S}$, then its inverse is $\inv{T}$.
\end{lemma}

\begin{proof}
	Since $T$ is an isomorphism, there exists a compatible subordination $Q \colon B_2 \to B_1$  such that $Q \circ T = S_1$ and $T \circ Q = S_2$.
As we pointed out in the proof of Lemma~\ref{l:functional-alternative-def},
	to show that $\inv{T} \circ T \subseteq S_1$ it is sufficient to prove that $a \mathrel{T} 0$ implies $a=0$ for each $a \in B_1$. Since $0 \mathrel{Q} 0$, we have that $a \mathrel{T} 0$ implies $a \mathrel{(Q \circ T)} 0$. Thus, $a \mathrel{S}_1 0$, and so $a=0$. We now show that $S_2 \subseteq T \circ \inv{T}$. Let $b_1,b_2 \in B_2$ be such that $b_1 \mathrel{S}_2 b_2$. By \eqref{S7}, there is $d \in B_2$ such that $b_1 \mathrel{S}_2 d \mathrel{S}_2 b_2$ and so $\neg d \mathrel{S}_2 \neg b_1$ by \eqref{S6}.
	 Since $T \circ Q =S_2$, there exist $a,c \in B_1$ such that $d \mathrel{Q} a$, $a \mathrel{T} b_2$, $\neg d \mathrel{Q} c$, and $c \mathrel{T} \neg b_1$. Thus, $1=(d \vee \neg d) \mathrel{Q} (a \vee c)$, and hence $1 \mathrel{(Q \circ T)} (a \vee c)$ because $1 \mathrel{T} 1$. Therefore, $1 \mathrel{S}_1 (a \vee c)$. It follows that $a \vee c = 1$, and so $\neg a \le c$. This gives $\neg a \le c \mathrel{T} \neg b_1$, so $\neg a \mathrel{T} \neg b_1$. Thus, $b_1 \mathrel{\inv{T}} a$ and $a \mathrel{T} b_2$, which yield $b_1 \mathrel{(T \circ \inv{T})} b_2$. Therefore, $S_2 \subseteq T \circ \inv{T}$.
	Since $T$ is an isomorphism, $\inv{T}$ is an isomorphism as well. Indeed, $\inv{T} \circ \inv{Q} = \inv{Q \circ T} = \inv{S_1} = S_1$ and similarly $\inv{Q} \circ \inv{T} = S_2$. By the argument above with $\inv{T}$ in place of $T$, we obtain
	\[
	T \circ \inv{T} =  \doubleinvT \circ \inv{T} \subseteq S_2 \quad \mbox{and} \quad S_1 \subseteq \inv{T} \circ \doubleinvT = \inv{T} \circ T.
	\]
	Thus, $\inv{T} \circ T = S_1$ and $T \circ \inv{T} = S_2$, and hence $\inv{T}$ is the inverse of $T$.
\end{proof}

\begin{lemma}\label{lem:functionality SI(T) and B(box)}
Let $(B_1,S_1),(B_2,S_2)$ be $\mathsf{S5}$-subordination algebras and $T \colon B_1 \to B_2$ a morphism in $\mathsf{SubS5^S}$. Let also $L_1,L_2$ be compact regular frames and $\Box \colon L_1 \to L_2$ a preframe homomorphism.
\begin{enumerate}[label=\normalfont(\arabic*), ref = \arabic*]
\item\label{lem:functionality SI(T) and B(box):item1} If $T \colon B_1 \to B_2$ is a functional compatible subordination, then ${\mathcal{SI}}(T) \colon {\mathcal{SI}}(B_2) \to {\mathcal{SI}}(B_1)$ is a frame homomorphism.
\item\label{lem:functionality SI(T) and B(box):item2} If $\Box \colon L_1 \to L_2$ is a frame homomorphism, then $\mathfrak{B}(\Box) \colon \mathfrak{B}L_2 \to \mathfrak{B}L_1$ is functional.
\item\label{lem:functionality SI(T) and B(box):item3} If $T \colon B_1 \to B_2$ is an isomorphism in $\mathsf{SubS5^S}$, then $T$ is an isomorphism in $\mathsf{SubS5^F}$.
\item\label{lem:functionality SI(T) and B(box):item4} If $\Box \colon L_1 \to L_2$ is an isomorphism in ${\mathsf{KRFrm^P}}$, then $\Box$ is an isomorphism in ${\mathsf{KRFrm}}$.
\end{enumerate}
\end{lemma}

\begin{proof}
	\eqref{lem:functionality SI(T) and B(box):item1}.
	Since $\mathcal{SI}(T)$ is a preframe homomorphism (see Proposition~\ref{prop:RI compact regular}), it is sufficient to prove that it preserves bottom and binary joins.
	To see that $\mathcal{SI}(T)$ preserves bottom, it is enough to show that
	$T^{-1}[\{0\}] \subseteq \{0\}$, which follows from
	Lemma~\ref{l:functional-alternative-def}\eqref{i:fun-0-ary}.
	To see that $\mathcal{SI}(T)$ preserves binary joins,
	let $I_1, I_2$ be S-ideals of $B_2$.
	It is sufficient to prove that $T^{-1}[I_1 \lor I_2] \subseteq T^{-1}[I_1] \lor T^{-1}[I_2]$.
	Let $a \in T^{-1}[I_1 \lor I_2]$.
	Then there are $b_1 \in I_1$, $b_2 \in I_2$ such that $a \mathrel{T} (b_1 \lor b_2)$.
	Since $I_1$ and $I_2$ are S-ideals, there are $b_1' \in I_1$ and $b_2' \in I_2$ such that $b_1 \mathrel{S}_2 b_1'$ and $b_2 \mathrel{S}_2 b_2'$.
	By Lemma~\ref{l:functional-alternative-def}\eqref{i:fun-2-ary}, there are $a_1, a_2 \in B_1$ such that $a \mathrel{S}_1 (a_1 \lor a_2)$, $a_1 \mathrel{T} b_1'$, and $a_2 \mathrel{T} b_2'$.
	Thus, $a \in T^{-1}[I_1] \lor T^{-1}[I_2]$.

	\eqref{lem:functionality SI(T) and B(box):item2}. We prove that $\mathfrak{B}(\Box)$ satisfies Lemma~\ref{l:functional-alternative-def}\eqref{i:new-functional}.
	To see \eqref{i:fun-0-ary}, let $b \in \mathfrak{B}L_2$ be such that $b \mathrel{\mathfrak{B}(\Box)}0$.
	By definition of $\mathrel{\mathfrak{B}(\Box)}$, we have $b \prec \Box 0=0$.
	Therefore, $b = 0$ by \eqref{S5}.
	To see \eqref{i:fun-2-ary},
	let $b \in \mathfrak{B}L_2$ and $a_1, a_2, a_1', a_2' \in \mathfrak{B}L_1$ be such that $b \mathrel{\mathfrak{B}(\Box)} (a_1 \lor a_2)$, $a_1 \prec a_1'$, and $a_2 \prec a_2'$.
	By definition of $\mathrel{\mathfrak{B}(\Box)}$, we have $b \prec \Box(a_1 \lor a_2)$. But $\Box(a_1 \lor a_2)=\Box a_1 \lor \Box a_2$ because $\Box$ is a frame homomorphism.
	Therefore, $b \prec \Box a_1 \lor \Box a_2$, and so there is $b' \in \mathfrak{B}(\Box)$ such that $b \prec b' \prec \Box a_1 \lor \Box a_2$.
	Set $b_1 = b' \land \Box a_1$ and $b_2 = b' \land \Box a_2$.
	We have $a_i \prec a_i'$ implies $\Box a_i \prec \Box a_i'$ for $i \in \{1, 2\}$.
	Thus, $b_i = b' \land \Box a_i \leq \Box a_i \prec \Box a_i'$, so $b_i \prec \Box a_i'$, and hence $b_i \mathrel{\mathfrak{B}(\Box)} a_i'$.
	Moreover, from $b \prec b'$ and $b \prec \Box a_1 \lor \Box a_2$ it follows that
	\[
	b \prec b' \land (\Box a_1 \lor \Box a_2) = (b' \land \Box a_1) \lor (b' \land \Box a_2) = b_1 \lor b_2.
	\]
	This proves \eqref{i:fun-2-ary}.

	\eqref{lem:functionality SI(T) and B(box):item3}.
	By Lemma~\ref{lem: inv of T}, the inverse of $T$ is $\inv{T}$.
	Since $\doubleinvT = T$ and $\inv{T}$ is the inverse of $T$, we have
	\[
	\doubleinvT \circ \inv{T} = T \circ \inv{T} = S_2 \quad \mbox{and} \quad S_1 = \inv{T} \circ T = \inv{T} \circ \doubleinvT.
	\]
	Therefore, $\inv{T}$ is functional. Thus, $T$ is an isomorphism in $\mathsf{SubS5^F}$.

	\eqref{lem:functionality SI(T) and B(box):item4}.
	Both in ${\mathsf{KRFrm^P}}$ and ${\mathsf{KRFrm}}$ isomorphisms are order-isomorphisms.
\end{proof}

From Theorems~\ref{thm: NI equivalence}, \ref{thm:dual-equivalence}, and Lemma~\ref{lem:functionality SI(T) and B(box)} we obtain:

\begin{theorem} \label{t:restriction-functional}
$ $
\begin{enumerate}[label=\normalfont(\arabic*), ref = \arabic*]
\item The equivalence between $\mathsf{SubS5^S}$ and $\mathsf{DeV^S}$ restricts to an equivalence between their wide subcategories $\mathsf{SubS5^F}$ and $\mathsf{DeV^F}$.
\item The dual equivalence between $\mathsf{SubS5^S}$ and ${\mathsf{KRFrm^P}}$ restricts to a dual equivalence between their wide subcategories $\mathsf{SubS5^F}$ and ${\mathsf{KRFrm}}$.
\item The dual equivalence between $\mathsf{DeV^S}$ and ${\mathsf{KRFrm^P}}$ restrict to a dual equivalence between their wide subcategories $\mathsf{DeV^F}$ and ${\mathsf{KRFrm}}$.
\end{enumerate}
\end{theorem}

As follows from \cite[Thm.~8.18]{ABC22}, ${\mathsf{DeV}}$ is dually isomorphic to $\mathsf{DeV^F}$. Thus, we arrive at the following analogue of the commutative diagram of equivalences and dual equivalences given at the end of Section~\ref{sec: cont subs}.
\[
\begin{tikzcd}[column sep=6ex, row sep=6ex]
& \mathsf{SubS5^F} \arrow[dl, "{\mathcal{SI}}"'] \arrow[dr, shift left=1ex, "{\mathcal{NI}}"] &  &\\
{\mathsf{KRFrm}} \arrow[rr, "{\mathfrak{B}}"] & & \mathsf{DeV^F} \arrow[ul, hookrightarrow, shift left=0.5ex, "\Delta"] \arrow[r, leftrightarrow, "d"] & {\mathsf{DeV}}
\end{tikzcd}
\]

Since $\mathsf{Comp^F}$ is a full subcategory of $\mathsf{SubS5^F}$ that contains $\mathsf{DeV^F}$, it follows that $\mathsf{Comp^F}$ is equivalent to both $\mathsf{SubS5^F}$ and $\mathsf{DeV^F}$, and hence dually equivalent to ${\mathsf{KRFrm}}$ and ${\mathsf{DeV}}$.

\begin{remark}
We recall from \cite[Def.~8.1]{ABC22} that a morphism $R\colon (X_1,E_1)\to (X_2,E_2)$ in $\mathsf{StoneE}^\mathsf{R}$ is {\em functional} if $E_1\subseteq \conv{R}\circ R$ and $R\circ\conv{R}\subseteq E_2$. Let $\mathsf{StoneE}^\mathsf{F}$ be the wide subcategory of $\mathsf{StoneE}^\mathsf{R}$ consisting of functional morphisms and define $\mathsf{Gle}$ similarly. By \cite[Thm.~8.8]{ABC22}, the categories $\mathsf{SubS5^F}$, $\mathsf{StoneE}^\mathsf{R}$, $\mathsf{Gle}$, and ${\mathsf{KHaus}}$  are equivalent. Thus, each of these is equivalent or dually equivalent to the categories in the above diagram.
\end{remark}

We thus arrive at the following diagram, in which empty boxes of the diagram at the end of Section~\ref{sec: prelims} are filled. Because of the lack of space, the equivalences and dual equivalences involving categories of compingent algebras are left out.
\[
\begin{tikzcd}[column sep=0.90cm]
\mathsf{SubS5^S} \arrow[r, leftrightarrow] & \mathsf{DeV^S} \arrow[rr, leftrightarrow, "d"] & & {\mathsf{KRFrm^P}} \arrow[r, leftrightarrow, "d"] & \mathsf{KHaus}^\mathsf{R} \arrow[r, leftrightarrow] & \mathsf{StoneE}^\mathsf{R} \arrow[r, leftrightarrow] & \mathsf{Gle}^\mathsf{R} \\
\mathsf{SubS5^{CS}} \arrow[u, hookrightarrow] \arrow[r, leftrightarrow] & \mathsf{DeV^{CS}} \arrow[u, hookrightarrow] \arrow[r, leftrightarrow, "d"] & \mathsf{DeV^C} \arrow[r, leftrightarrow] & {\mathsf{KRFrm^C}} \arrow[u, hookrightarrow] \arrow[r, leftrightarrow, "d"] & \mathsf{KHaus}^\mathsf{C} \arrow[u, hookrightarrow] \arrow[r, leftrightarrow] & \mathsf{StoneE}^\mathsf{C} \arrow[u, hookrightarrow] \arrow[r, leftrightarrow] & \mathsf{Gle}^\mathsf{C} \arrow[u, hookrightarrow] \\
\mathsf{SubS5^F} \arrow[u, hookrightarrow] \arrow[r, leftrightarrow] & \mathsf{DeV^F} \arrow[u, hookrightarrow] \arrow[r, leftrightarrow, "d"] & {\mathsf{DeV}} \arrow[u, hookrightarrow] \arrow[r, leftrightarrow] & {\mathsf{KRFrm}} \arrow[u, hookrightarrow] \arrow[r, leftrightarrow, "d"] & {\mathsf{KHaus}} \arrow[u, hookrightarrow] \arrow[r, leftrightarrow] & \mathsf{StoneE}^\mathsf{F} \arrow[u, hookrightarrow] \arrow[r, leftrightarrow] & \mathsf{Gle} \arrow[u, hookrightarrow]
\end{tikzcd}
\]

\section*{Acknowledgements}
Marco Abbadini and Luca Carai were supported by the Italian Ministry of University and Research through the PRIN project n.\ 20173WKCM5 \emph{Theory and applications of resource sensitive logics}.

redpajama_set_name: RedPajamaArXiv