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.

tightapartness relations, right? BTW is there a name for objects $X$ with $\neg\neg$-dense diagonal? I didn't realize there was a condition like this on the equality relation intermediate between decidability and non-decidability... $\endgroup$ – Tim Campion♦ Feb 23 '20 at 16:013more comments