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.
Moved “Application” section from the decidable equality article to this article since the statements made in the section are only true if and only if the sets with decidable equality additionally have decidable tight apartness.
Otherwise, stuff like Heyting fields are still important in basic algebra, because one can have fields with decidable equality along with its tight apartness that does not coincide with the negation of equality, such as the Dedekind real numbers with analytic WLPO.
Anonymouse
1 to 2 of 2