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 $X$ has stable equality if any two elements of $X$ are equal if (hence iff) they are not not equal.

Examples
Every set with decidable equality has stable equality, but not conversely.

Every set $S$ with a tight apartness relation $\#$ has stable equality, because even in constructive mathematics , given elements $x \in S$ and $y \in S$ , $\neg \neg \neg (x \# y) \iff \neg (x \# y)$ , and because $\neg (x \# y) \iff x = y$ , $\neg \neg (x = y) \iff x = y$ , and thus $S$ 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.