Pointfree reloids discovered

After I defined pointfree funcoids which generalize funcoids (see my draft book) I sought for pointfree reloids (a suitable generalization of reloids, see my book) long time.

Today I have finally discovered pointfree reloids. The idea is as follows:

Funcoids between sets $latex A$ and $latex B$ denoted $latex \mathsf{FCD}(A;B)$ are essentially the same as pointfree funcoids $latex \mathsf{pFCD}(\mathfrak{F}(A);\mathfrak{F}(B))$ (where $latex \mathfrak{F}(A)$ denotes filters on a set $latex A$).

Reloids between sets $latex A$ and $latex B$ denoted $latex \mathsf{RLD}(A;B)$ are essentially the same as filters $latex \mathfrak{F}(\mathbf{Rel}(A;B))$ (where $latex \mathbf{Rel}$ is the category of binary relations between sets.)

But, as I’ve recently discovered (see my book), $latex \mathbf{Rel}(A;B)$ is essentially the same as $latex \mathsf{pFCD}(\mathscr{P}A;\mathscr{P}B)$. So $latex \mathsf{RLD}(A;B) = \mathfrak{F}(\mathbf{pFCD}(\mathscr{P}A;\mathscr{P}B))$.

This way (for every posets $latex \mathfrak{A}$, $latex \mathfrak{A}$) $latex \mathfrak{F}\mathbf{pFCD}(\mathscr{A};\mathscr{B})$ corresponds to $latex \mathbf{pFCD}(\mathfrak{F}(\mathscr{A});\mathfrak{F}(\mathscr{B}))$ in the same way as $latex \mathsf{RLD}(A;B)$ corresponds to $latex \mathsf{FCD}(A;B)$. In other words, $latex \mathfrak{F}\mathbf{pFCD}(\mathscr{A};\mathscr{B})$ are the pointfree reloids corresponding to pointfree funcoids $latex \mathbf{pFCD}(\mathfrak{F}(\mathscr{A});\mathfrak{F}(\mathscr{B}))$.

Yeah!