nLab
stable equality
Contents
Context
Equality and Equivalence
equivalence
-
equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
-
identity type, equivalence in homotopy type theory
-
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
-
natural equivalence, natural isomorphism
-
gauge equivalence
-
Examples.
principle of equivalence
equation
-
fiber product, pullback
-
homotopy pullback
-
Examples.
-
linear equation, differential equation, ordinary differential equation, critical locus
-
Euler-Lagrange equation, Einstein equation, wave equation
-
Schrödinger equation, Knizhnik-Zamolodchikov equation, Maurer-Cartan equation, quantum master equation, Euler-Arnold equation, Fuchsian equation, Fokker-Planck equation, Lax equation
Foundations
foundations
The basis of it all
-
mathematical logic
-
deduction system, natural deduction, sequent calculus, lambda-calculus, judgment
-
type theory, simple type theory, dependent type theory
-
collection, object, type, term, set, element
-
equality, judgmental equality, typal equality
-
universe, size issues
-
higher-order logic
Set theory
Foundational axioms
Removing axioms
Contents
Definition
In constructive mathematics, a set has stable equality if any two elements of are equal if (hence iff) they are not not equal.
Examples
-
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.
-
Since every Heyting field has a tight apartness relation and thus stable equality, every nilpotent element is equal to zero.
-
In particular, the Dedekind real numbers have stable equality, and any Heyting subfield of the Dedekind real numbers has stable equality.
See also
References
Last revised on December 8, 2022 at 16:32:31.
See the history of this page for a list of all contributions to it.