Apartness relation

Let $𝑋$ be a collection. An apartness relation $(#)$ on $𝑋$ is a relation satisfying laws complementary to that of an equivalence relation #m/def/set

irreflexivity $\neg (𝑥 # 𝑥)$
symmetry $𝑥 # 𝑦 \to 𝑦 # 𝑥$
cotransitivity $𝑥 # 𝑧 \to (𝑥 # 𝑦) \lor (𝑦 # 𝑧)$

An apartness relation on a fibrant type is tight iff it additionally satisfies

tightness $\neg (𝑥 # 𝑦) \to 𝑥 = 𝑦$

A type equipped with a tight apartness relation is called an aset. Every aset has DN-stable equality, and thus is in particular, an h-set by Hedberg’s theorem.

Proof

Suppose $\neg \neg (𝑥 = 𝑦)$ . Then it is not the case that $𝑥 # 𝑦$ , for if it were then we would have $\neg (𝑥 = 𝑦)$ by irreflexivity. Hence by tightness we have $𝑥 = 𝑦$ .

Classically asets are boring, and apartness relations are precisely the complements of equivalence relations.

#state/develop | #lang/en | #SemBr