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.