Really just add the identities defining a pointfree funcoid to the identities of an upper semilattice with least element.
I will list the exact list of identities defining a pointfree funcoid on a poset with least element:
- $latex x \leq x$
- $latex x \leq y \land y \leq z \Rightarrow x \leq z$
- $latex x \leq y \land y \leq x \Rightarrow x=y$
- $latex \bot \leq y$
- $latex \lnot(\bot [f] y)$
- $latex \lnot(x [f] \bot)$
- $latex x \cup y \leq z \Leftrightarrow x \leq z \land y \leq z$
- $latex i\cup j[f]k \Leftrightarrow i[f]k\lor j[f]k$
- $latex k[f]i\cup j \Leftrightarrow k[f]i\lor k[f]j$
(Here $latex [f]$ is a single relational symbol.)
This can be even generalized for upper semilattices with no requirement to have the least element, if we allow the least element constant symbol to be a partial function.
Note that for the general case of a pointfree funcoid between two upper semilattices, we have a partial algebraic structure because the operations are different for each of the two upper semilattices.
I am curious what are applications of this curious fact.