It seems apartness composition fails to form the following categorical structures:
-
•
Monoidal Category With Products. Products don’t seem to endow $\mathsf{Rel}^{\mathord {\mathbin {\square }}}$ with a monoidal structure.
-
•
Monoidal Category With Coproducts. Coproducts also don’t seem to endow $\mathsf{Rel}^{\mathord {\mathbin {\square }}}$ with a monoidal structure.
-
•
Double Categorical Structure. It seems the apartness composition of relations doesn’t form a double category in a natural1 way.
- 1I.e. such that the composition of vertical morphisms is the usual composition of functions, as in $\mathsf{Sets}$.
