Added fact that the category of inequality spaces has a real numbers object given by the Dedekind real numbers.

Anonymouse

]]>Removed the sentence about Hedberg’s theorem. As discussed in this Mastodon thread, the statement taken at face value is false (the reals are an example of a type with a tight apartness relation that does not have decidable equality), and there doesn’t seem to be a way to salvage it as it seems to have gotten the hypothesis and conclusion of Hedberg’s theorem backwards.

]]>moving material on inequality spaces from apartness relation to here.

Anonymous

]]>