A tight apartness relation on a set is a binary relation $\#$ such that the following conditions hold:
- $x = y$ if and only if $\neg (x \# y)$.
- If $x \# y$, then $y \# x$.
- If $x \# z$, then either $x \# y$ or $y \# z$ for every $y$.
I want to understand this notion better. Classically, it is completely trivial. Thus, it makes sense to look at it in various toposes. I tried to use the Kripke-Joyal semantics to get the external interpretation of an arbitrary object of a topos with a tight apartness relation, but it seems that it does not give anything particularly interesting in general. Thus, I've got the following question:
Question: What are examples of objects in toposes with a tight apartness relation which externally correspond to some interesting or useful notion?
Since constructively, a set can have more than one tight apartness relation on it, I'd like to see examples of an object with two different tight apartness relations which both have interesting interpretations.
Edit: There are several "generic" examples of objects with tight apartness relations, i.e., objects that can be defined in every topos (e.g., Dedekind reals). I'm particularly interested in "non-generic" examples, i.e., objects that can be constructed only in a specific topos.