It is not difficult to prove (see “Counter-examples about funcoids and reloids” in the book) that $latex 1^{\mathsf{FCD}} \sqcap^{\mathsf{FCD}} (\top\setminus 1^{\mathsf{FCD}}) = \mathrm{id}^{\mathsf{FCD}}_{\Omega}$ (where $latex \Omega$ is the cofinite filter). But the result is counterintuitive: meet of two binary relations is not a binary relation.

After proving this I always felt that there is some “mystery” about meet of funcoids: It behaves in a weird way and what it is in general (not this one special counterexample case) is not known.

Today I noted a simple formula which decomposes $latex f \sqcap^{\mathsf{FCD}} g$: $latex f \sqcap^{\mathsf{FCD}} g = (\mathsf{FCD})((\mathsf{RLD})f \sqcap (\mathsf{RLD})g)$ for every funcoids $latex f$ and $latex g$ and more generally $latex \bigsqcap^{\mathsf{FCD}} S = (\mathsf{FCD}) \bigsqcap^{\mathsf{RLD}} \langle (\mathsf{RLD})_{\mathrm{in}} \rangle^{\ast} S$ for a set $latex S$ of funcoids. (It follows from that $latex (\mathsf{FCD})$ is an upper adjoint and that $latex (\mathsf{FCD})(\mathsf{RLD})_{\mathrm{in}} f=f$ for every funcoid $latex f$.) This way it looks much more clear and less counterintuitive.

So now it looks more clear, but I have not yet found particular implications of these formulas leading to interesting results.