Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Apartness relations

Madeleine Birchfield (Feb 01 2024 at 16:49):

Suppose a set $A$ has a tight apartness relation $R:\neq_A \to A \times A$. Is the tight apartness relation the terminal apartness relation on $A$, in the sense that for any other apartness relation $R_\#:\# \to A \times A$ there exists a unique function $u:\# \to \neq_A$ which preserves being an apartness relation such that $R \circ u = R_\#$?

Ralph Sarkis (Feb 01 2024 at 17:22):

I would say yes. What does "which preserves being an apartness relation" mean? If it is something more than the equation you wrote, I would say it is unnecessary.

Ralph Sarkis (Feb 01 2024 at 17:28):

The way I understand it is that a tight apartness relation is inequality. An apartness relation is the complement of an equivalence relation. Any equivalence relation contains equality which is the complement of inequality, hence any apartness relation is contained in inequality.

Madeleine Birchfield (Feb 01 2024 at 17:38):

Ralph Sarkis said:

The way I understand it is that a tight apartness relation is inequality. An apartness relation is the complement of an equivalence relation. Any equivalence relation contains equality which is the complement of inequality, hence any apartness relation is contained in inequality.

I forgot to mention that I am working in constructive mathematics here. There is a difference between inequality as negation of equality and a tight apartness relation in constructive mathematics, because without excluded middle one cannot prove that the negation of equality is either tight or cotransitive.

Mike Shulman (Feb 01 2024 at 21:51):

If this were true, then a tight apartness on a set would be unique if it exists, but this isn't the case. For instance, let $P$ be a proposition, and $2_P$ be the quotient/HIT set with two elements $a,b$ such that $(a=b) \leftrightarrow P$. Then an apartness on $2_P$ is determined by a proposition $Q \coloneqq (a\#b)$ such that $P\wedge Q = \bot$, and it is tight iff $\neg Q \to P$. In general there could be many such $Q$.