equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
identity type, equivalence of types, definitional isomorphism
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
basic constructions:
strong axioms
further
In constructive mathematics, a set has stable equality if any two elements of are equal if (hence iff) they are not not equal.
Every set with decidable equality has stable equality, but not conversely.
Every set with a tight apartness relation has stable equality, because even in constructive mathematics, given elements and , , and because , , and thus is stable.
In particular, the Dedekind real numbers have stable equality, and any Heyting subfield of the Dedekind real numbers has stable equality.
Last revised on November 28, 2023 at 03:09:42. See the history of this page for a list of all contributions to it.