Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
1 to 2 of 2