Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
An apartness relation is a binary relation that, instead of saying when two things are the same (as an equivalence relation), states when two things are different – an inequality relation.
Apartness relations are most used in constructive mathematics; in classical mathematics, equivalence relations can take their place (mediated by negation).
The apartness relations that we discuss here are sometimes called point–point apartness, to distinguish this from the set–set apartness relation between subsets of an apartness space? (which is related).
A set $S$ equipped with an apartness relation is a groupoid (with $S$ as the set of objects) enriched over the cartesian monoidal category $TV^\op$, that is the opposite of the poset of truth values, made into a monoidal category using disjunction. By the law of excluded middle (which says that $TV$ is self-dual under negation), this is equivalent to equipping $S$ with an equivalence relation (which makes $S$ a groupoid enriched over the cartesian category $TV$ itself). But in constructive mathematics (or interpreted internally), it is a richer concept with a topological flavour.
Of course, nobody but a category-theorist would use the above as a definition of an apartness relation. Normally, one defines an apartness relation on $S$ as a binary relation $\#$ satisfying these three properties:
(Notice that these are dual to the axioms for an equivalence relation; like those axioms, these correspond to identity morphisms, inverses, and composition in a groupoid.)
The negation of an apartness relation is an equivalence relation. (The converse of this is equivalent to excluded middle.) An apartness relation is tight (see connected relation) if this equivalence relation is equality; any apartness relation defines a tight apartness relation on the quotient set. A tight apartness relation, also called an inequality, is often written $\ne$ instead of $\#$, but keep in mind that $\ne$ is not the negation of $=$; rather, $=$ is the negation of $\ne$. (So inequality, when it exists, is more basic than equality.)
If $S$ and $T$ are both sets equipped with apartness relations, then a function $f\colon S \to T$ is strongly extensional if $x \# y$ whenever $f(x) \# f(y)$; that is, $f$ reflects apartness. The strongly extensional functions are precisely the enriched functors between $TV^\op$-enriched groupoids, so they are the correct morphisms. (Note that there is no nontrivial notion of enriched natural isomorphism, at least not when the apartness in $T$ is tight.)
By an inequality space, I mean a set equipped with a tight apartness relation. By a map, I mean a strongly extensional function between inequality spaces.
The category of inequality spaces has all (small) limits, created by the forgetful functor to Set. (For example, $(a,b) \ne (x,y)$ iff $a \ne x$ or $b \ne y$.) Similarly, it has all finite coproducts, and it has quotients of equivalence relations. In fact, this category is a complete pretopos. It is not, however, a Grothendieck topos (or even a topos at all), because it doesn't have all infnite coproducts. (To be precise, the statement that it has all small coproducts, or even that it has a subobject classifier, seems to be equivalent to excluded middle.)
We can say, however, that it has coproducts indexed by inequality spaces, although to make this precise is a triviality. More interestingly, it has products indexed by inequality spaces; that is, it is (even locally) a cartesian closed category. In particular, given inequality spaces $X$ and $Y$, the set $\StrExt(X,Y)$ of maps from $X$ to $Y$ becomes an inequality space under the rule that $f \ne g$ iff $f(x) \ne g(x)$ for some $x\colon X$.
If you generalise from inequality spaces to allow non-tight apartness relations, then you get (at first) a different category. However, now you also have $2$-morphisms which serve to identify unequal but equivalent (that is, not apart) elements of a space, so the resulting bicategory is equivalent to the category of inequality spaces.
Let $S$ be a set equipped with a tight apartness relation $\ne$. Using $\ne$, many topological notions may be defined on $S$. (It's not really necessary that the apartness be tight; this corresponds to the $T_0$ separation axiom in topology.)
If $U$ is a subset of $S$ and $x$ is an element, then $U$ is a $\ne$-neighbourhood (or $\ne$-neighborhood) of $x$ if, given any $y\colon S$, $x \ne y$ or $y \in U$; note that $x \in U$ by irreflexivity. The neighbourhoods of $x$ form a filter: a superset of a neighbourhood is a neigbhourhood, and the intersection of $0$ or $2$ (hence of any finite number) of neighbourhoods is a neighbourhood.
A subset $G$ is $\ne$-open if it's a neighbourhood of all of its members. The open subsets form a topology (in the sense of Bourbaki): any union of open subsets is open, and the intersection of $0$ or $2$ (hence of any finite number) of open subsets is open.
The $\ne$-complement of $x$ is the subset $\{y\colon S \;|\; x \ne y\}$; this is open by comparison. More generally, the $\ne$-complement of any subset $A$ is the set $\tilde{A}$, defined as:
This is not in general open, but you would use it where you would classically use the set-theoretic complement. However, if $A$ is open to begin with, then $\tilde{A}$ equals the set-theoretic complement.
If $x \ne y$, then $x \in \tilde{y}$ and $y \in \tilde{x}$, which shows that $(S, \ne)$ satisfies the $T_1$ separation axiom. Symmetry is important here; if we removed symmetry from the axioms of apartness, then we would still get a $T_0$ topology, but it would not be $T_1$. This is a version of the fact that failure of $T_1$ is given by a partial order (or a preorder if $T_0$ might also fail).
The $\ne$-closure $\bar{A}$ of a subset $A$ is the complement of its complement. This closure is a closure operator: $A \subset \bar{A}$, $\overline{\bar{A}} = \bar{A}$ (in fact, $\overline{\tilde{A}} = \tilde{A}$), $\bar{A} \subset \bar{B}$ whenever $A \subset B$, $\overline{S} = S$ (in fact, $\bar{\empty} = \empty$ too), and $\overline{A \cap B} = \bar{A} \cap \bar{B}$ (but not $\overline{A \cup B} = \bar{A} \cup \bar{B}$).
The antigraph of a function $f\colon S \to T$ is
Recall that in ordinary topology, a function between Hausdorff spaces is continuous iff its graph is closed. Similarly, a function $f\colon S \to T$ is strongly extensional iff its antigraph is open. (Then the graph of $f$ is the complement of the antigraph.)
One important topological concept that doesn't appear classically is locatedness; in an inequality space, a subset $A$ is located if, given any point $x$ and any neighbourhood $U$ of $x$, either $U \cap A$ is inhabited (that is, it has a point) or some neighbourhood of $x$ (not necessarily $U$) is contained in $\tilde A$. Note that every point is located. (For an example of a set that need not be located, consider $\{x\colon S \;|\; p\}$, where $p$ is an arbitrary truth value. In an inhabited space, this set is located iff $p$ is true or false.)
Recall that, as Bill Lawvere taught us, a metric space is a groupoid (or $\dag$-category) enriched over the category $([0,\infty[^\op,+)$ of nonnegative real numbers, ordered in reverse, and made monoidal under addition. (Actually, you get a metric only if you impose a tightness condition, although again you can recover this up to equivalence from the $2$-morphisms. Furthermore, Lawvere advocated using $[0,\infty]$ instead of $[0,\infty[$, and also dropping the symmetry requirement to get enriched categories instead of groupoids. Thus, he dealt with extended quasipseudometric spaces. These details are not really important here.)
There is a monoidal functor from $([0,\infty[^\op,+)$ to $TV^\op$ that maps a nonnegative real number $x$ to the truth value of the statement that $x \gt 0$. Accordingly, any (symmetric) metric space becomes an inequality space, and any function satisfying $d(f(x),f(y)) \leq d(x,y)$) is strongly extensional.
The topological properties of metric spaces fit well with those of inequality spaces if you always work in this direction. For example, a set which is $d$-open will also be $\ne$-open, but not necessarily the other way around. Similarly, a (merely) continuous function between metric spaces is (still) strongly extensional.
In analysis, many spaces are given as gauge spaces, that is by families of pseudometrics; these also become inequality spaces by declearing that $x \ne y$ iff $d(x,y) \gt 0$ for some pseudometric $d$ in the family. (This will actually be a tight apartness iff the family of pseudometrics is separating.) Classically, any uniform space may be given by a family of pseudometrics, but this doesn't hold constructively. In particular, a topological group may not be an inequality group (as in the next section).
The constructive theory of proximity spaces is based on a generalisation of apartness relations (which here go between points) to an apartness relation between sets. These are called apartness spaces?; just as apartness relations (between points) are classically equivalent to equivalence relations, so apartness spaces are classically equivalent to proximity spaces, with two sets being proximate if and only if they are not apart.
Of course, any apartness space has an apartness relation between points: $x$ and $y$ are apart iff $\{x\}$ and $\{y\}$ are apart.
Since inequality spaces have finite limits, the usual constructions of universal algebra apply; it's straightforward to define inequality groups, inequality rings, and so on.
The various subsets that appear in algebra (such as ideals and cosets) become less fundamental than certain subsets that are, classically, simply their complements. For example, a left ideal in a ring $R$ is a subset $I$ such that $0 \in I$, $x + y \in I$ whenever $x, y \in I$, and $x y \in I$ whenever $x \in I$. But a left antiideal in $R$ is a subset $A$ such that $0 \in A$ is false, $x \in A$ or $y \in A$ whenever $x + y \in A$, and $x \in A$ whenever $x y \in A$. Notice that an antiideal is necessarily $\ne$-open (using that the ring operations are strongly extensional), and its complement is an ideal. But the converse of this is not constructively valid, so antiideals are more fundamental than ideals, in an inequality ring.
Prime ideals are even more interesting. A two-sided antiideal $A$ (so also satisfying that $y \in A$ whenever $x y \in A$) is antiprime if $1 \in A$ and $x y \in A$ whenever $x, y \in A$. Now the complement of an antiprime antiideal may not be a prime ideal (as normally defined). But in fact, it is antiprime antiideals that are more important in constructive algebra. In particular, an integral domain in constructive algebra is an inequality ring in which the antiideal of nonzero elements is antiprime.
The notion of apartness as fundamental in metric spaces may be found in Errett Bishop’s Foundations of Constructive Analysis (1967) (or the 1985 edition with Douglas Bridges, Constructive Analysis). But as I recall, this doesn't introduce the concept in general; that came in Anne Troelstra's and Dirk van Dalen's Constructivism in Mathematics (1988). For apartness in algebra, see A Course in Constructive Algebra (also 1988), by Ray Mines, Fred Richman, and Wim Ruitenburg. A great reference for point-set topology in constructive mathematics is the Ph.D. thesis of Frank Waaldijk, Modern Intuitionist Topology (1996). Please note that I (Toby Bartels) have not read the algebra book.
Urs says: What you say at the entry vector space about the relation between apartness relations and topology and the continuum sounds very interesting. It would be nice if you could move these comments here and maybe flesh them out a little. Because, while it sounds interesting, I don’t yet understand what you are saying!
Toby replies: I will try to write a bit about the topological ideas that come up. But keep in mind that classically it is all trivial, unless you rephrase it internal to some more general notion of category than a boolean topos, and these things are not normally so phrased.
Urs replies to the reply: Okay, I’ll keep it in mind. But I am still interested! :-)
I already have problems with the above definition. When you say “coproduct” do you mean to equip $\{true, false\}$ with the monoidal structure given by logical OR? This is the only meaning I can give this word here, but a category enriched over $(\{true, false\},\otimes = OR)$ seems necessarily to be an indiscrete groupoid over its set of objects. (Because $hom(a,a) = true$ for all objects $a$ and then $hom(a,b) = hom(a,a) OR hom(a,b) = true$, too, for all $b$.)
Toby replies: To begin with, I defined it incorrectly; the trouble with these slick category-theoretic definitions is that a small error makes things completely messed up! I rephrased it quite a bit, but the key point is the new word ‘opposite’. That said, your analysis of even my original definition is unsound; keep in mind that the unit of disjunction is false.
Toby adds: Also, it's an enriched groupoid, not an enriched category.
I am also not sure in which sense you refer to the law of the excluded middle. Should we maybe more generally say that the 0-category of (-1)-categories internal to a given topos $T$ is the subobject classifier, $(-1)Cat := \Omega$?
Toby replies: Yes, that is correct; $(-1)\Cat = \Omega$. Even when $T := \Set$, you have $(-1)\Cat = \{\top, \bot\}$ only if you believe excluded middle, which constructivists do not. Thus, constructivists will talk about apartness relations in $\Set$, while a classical mathematician will have to put the discussion internal to $T$ to get nontrivial results.
Urs replies to the reply: I like this statement “$(-1)\Cat = \Omega$”. Would we also want to say $(-2)Cat = \{1 \stackrel{\top}{\to} \Omega\}$?