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 and denoted are essentially the same as pointfree funcoids (where denotes filters on a set ).
Reloids between sets and denoted are essentially the same as filters (where is the category of binary relations between sets.)
But, as I’ve recently discovered (see my book), is essentially the same as . So .
This way (for every posets , ) corresponds to in the same way as corresponds to . In other words, are the pointfree reloids corresponding to pointfree funcoids .