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.

  • $\begingroup$ I'm a little out of my depth here, but I think the first bullet point tells you that in a topos, any object admitting an apartness relation must have decidable equality. I think the first two toposes I tend to think of besides $Set$ are $sSet$ and sheaves on a topological space $X$. In $sSet$, I think maybe only discrete objects have decidable equality? And in $Sh(X)$, maybe it's just coproducts of representables on clopen sets? $\endgroup$ – Tim Campion Feb 23 '20 at 6:48
  • 1
    $\begingroup$ The relation with the Hausdorff topology may be helpful. $\endgroup$ – Bas Spitters Feb 23 '20 at 11:48
  • 2
    $\begingroup$ @TimCampion It does not imply decidability of equality, it only implies that it is $\neg \neg$-separated. There are plenty of examples of objects with an apartness relation and without decidable equality. E.g., functions $\mathbb{N} \to \mathbb{N}$ and Dedekind reals. $\endgroup$ – Valery Isaev Feb 23 '20 at 13:46
  • $\begingroup$ @ValeryIsaev: Can you clarify? The condition "$\forall x,y : M. \neg\neg(x = y) \Rightarrow x = y$", interpreted in the internal language, is exactly the condition for the object $M$ to be separated with respect to the $\neg\neg$-topology. $\endgroup$ – Ingo Blechschmidt Feb 23 '20 at 15:48
  • $\begingroup$ @ValeryIsaev Surely you're right. Just to clarify (since it's the "tight"-ness part that has me confused more so than the "apartness" part), you're saying that in a topos, $\mathbb N^{\mathbb N}$ and $\mathbb R$ have tight apartness 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:01

I'm not precisely sure what you're looking for. Here is an example for the external interpretation of an apartness relation:

Recall that the object of Dedekind reals $\mathbb{R}$ in a sheaf topos $\mathrm{Sh}(X)$ is the sheaf $\mathcal{C}$ of continuous (Dedekind-)real-valued functions on $X$.

The apartness relation on $\mathbb{R}$, defined by $x \mathrel{\#} y \Longleftrightarrow x - y \text{ is invertible}$, is then the following subsheaf $\mathcal{E}$ of $\mathcal{C} \times \mathcal{C}$:

$$ \mathcal{E}(U) = \{ (f,g) \,|\, \text{for all $x \in U$: $f(x) - g(x) \in \mathbb{R}$ is invertible} \} $$

  • 2
    $\begingroup$ I'd like to see more examples like this one, but I think even more interesting are non-generic examples. That is, objects with tight apartness relations that can be constructed only in some particular topos (here, $\mathbb{R}$ can be constructed in any topos). $\endgroup$ – Valery Isaev Feb 23 '20 at 16:55
  • $\begingroup$ @ValeryIsaev I think it would be a good idea to include this requirement into your question. $\endgroup$ – Martin Brandenburg Feb 23 '20 at 19:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.